On Sun, Aug 4, 2013 at 1:29 PM, Florian Haftmann < [email protected]> wrote:
> 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. That's a great idea! I definitely wouldn't have thought about the AFP for a while. > My personal favorite is the lattice > development in > http://sourceforge.net/p/afp/code/ci/default/tree/thys/JinjaThreads/DFA/. > Thank you for the recommendation. I'll take a look =) > > Cheers, > Florian > > -- > > PGP available: > > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > >
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
