[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style

[Josh Tilles]

On Sun, Aug 4, 2013 at 1:29 PM, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:

> Hi Josh,
>
> > QUESTION STATED BRIEFLY:
> > If I convert existing proofs in src/HOL/**.thy from apply-style to
> > Isar-style, would those changes be welcome in the main repository?
>
> beyond the general hints given by Makarius, you could go the following way:
>
> a) Find a nice example (section) in theories sources.
> b) Do a quick plausibility check that there has been no movement in the
> repository tip concerning that particular example(s)
> (http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL).
> c) Post a announcement here.
> d) If nobody objects, go ahead and isarify.
> e) Post the resulting refinement here.
>
> Also note that if you want to practice Isar, there are also plenty of
> AFP theories which would profit from isarification and are a less
> critical point to start with.

That's a great idea! I definitely wouldn't have thought about the AFP for a
while.

>  My personal favorite is the lattice
> development in
> http://sourceforge.net/p/afp/code/ci/default/tree/thys/JinjaThreads/DFA/.
>
Thank you for the recommendation. I'll take a look =)

>
> Cheers,
>         Florian
>
> --
>
> PGP available:
>
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130916/7bd0e439/attachment-0002.html>