[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style
merelyapseudonym at gmail.com
Tue Jul 30 19:40:04 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?
>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...
More information about the isabelle-dev