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

[Florian Haftmann]

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.  My personal favorite is the lattice
development in
http://sourceforge.net/p/afp/code/ci/default/tree/thys/JinjaThreads/DFA/.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130804/b51a8a5b/attachment.asc>