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 <[email protected]> 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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
