[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style
merelyapseudonym at gmail.com
Tue Sep 17 04:08:53 CEST 2013
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)
> 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
> My personal favorite is the lattice
> development in
Thank you for the recommendation. I'll take a look =)
> PGP available:
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev