<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Aug 4, 2013 at 1:29 PM, Florian Haftmann <span dir="ltr"><<a href="mailto:florian.haftmann@informatik.tu-muenchen.de" target="_blank">florian.haftmann@informatik.tu-muenchen.de</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Josh,<br>
<div class="im"><br>
> QUESTION STATED BRIEFLY:<br>
> If I convert existing proofs in src/HOL/**.thy from apply-style to<br>
> Isar-style, would those changes be welcome in the main repository?<br>
<br>
</div>beyond the general hints given by Makarius, you could go the following way:<br>
<br>
a) Find a nice example (section) in theories sources.<br>
b) Do a quick plausibility check that there has been no movement in the<br>
repository tip concerning that particular example(s)<br>
(<a href="http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL" target="_blank">http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL</a>).<br>
c) Post a announcement here.<br>
d) If nobody objects, go ahead and isarify.<br>
e) Post the resulting refinement here.<br>
<br>
Also note that if you want to practice Isar, there are also plenty of<br>
AFP theories which would profit from isarification and are a less<br>
critical point to start with.</blockquote><div>That's a great idea! I definitely wouldn't have thought about the AFP for a while.</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

  My personal favorite is the lattice<br>
development in<br>
<a href="http://sourceforge.net/p/afp/code/ci/default/tree/thys/JinjaThreads/DFA/" target="_blank">http://sourceforge.net/p/afp/code/ci/default/tree/thys/JinjaThreads/DFA/</a>.<br></blockquote><div>Thank you for the recommendation. I'll take a look =) </div>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Cheers,<br>
        Florian<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
<br>
PGP available:<br>
<a href="http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de" target="_blank">http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de</a><br>


<br>
</font></span></blockquote></div><br></div></div>