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
