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

[Lawrence Paulson]

This could be a valuable service, especially for long lists of applys. (A proof like "by (induct n) auto" should be left alone.)

Do ask an experienced user to examine your early attempts for beginner's mistakes, like labelling all intermediate results.

Larry

On 30 Jul 2013, at 18:40, Josh Tilles <merelyapseudonym at gmail.com> wrote:

> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130730/cfdb052e/attachment-0002.html>