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

[Josh Tilles]

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?

EXPLANATION/DETAIL:
>From what I've read in the documentation, structured Isar proofs are
preferred over apply-style proofs in every case except for
prototyping/experimentation. (please let me know if I'm wrong about this
observation)
If newcomers to Isabelle/HOL "refactor" the lemmas & theories that were
written in the apply-style, presumably that frees the experienced
developers to spend their time on more creative endeavors.
*My* goals: I want to learn more about the conceptual organization of
Isabelle/HOL; and I want to make more of the implementation code
demonstrate idiomatic Isar, thus giving Isabelle beginners many more
examples to read and learn from.

--Josh
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130730/85f963e0/attachment.html>