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

Josh Tilles merelyapseudonym at gmail.com
Tue Jul 30 19:40:04 CEST 2013

If I convert existing proofs in src/HOL/**.thy from apply-style to
Isar-style, would those changes be welcome in the main repository?

>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
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.

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

More information about the isabelle-dev mailing list