[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style
florian.haftmann at informatik.tu-muenchen.de
Sun Aug 4 19:29:27 CEST 2013
> 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. My personal favorite is the lattice
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev