Hi Josh, > 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?
beyond the general hints given by Makarius, you could go the following way: a) Find a nice example (section) in theories sources. b) Do a quick plausibility check that there has been no movement in the repository tip concerning that particular example(s) (http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL). c) Post a announcement here. d) If nobody objects, go ahead and isarify. e) Post the resulting refinement here. Also note that if you want to practice Isar, there are also plenty of AFP theories which would profit from isarification and are a less critical point to start with. My personal favorite is the lattice development in http://sourceforge.net/p/afp/code/ci/default/tree/thys/JinjaThreads/DFA/. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
