<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jul 31, 2013 at 9:55 AM, Makarius <span dir="ltr"><<a href="mailto:makarius@sketis.net" target="_blank">makarius@sketis.net</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Tue, 30 Jul 2013, Josh Tilles wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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>
</blockquote>
<br></div>
It depends which part of the repository are affected.  To get changes accepted, someone who is an "expert" on that area of sources needs to apply them.  Finding out works by broadcasting here on this mailing list.</blockquote>

<div>That sounds perfectly reasonable. Should I share my changes by just attaching patches the "broadcasting" emails? </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

 (Changes in main HOL are always critical, since almost everything else depends on it, also performance-wise.)</blockquote><div>Interesting—I had assumed that changing the proof of a lemma and/or theorem had no functional impact on the code once said lemma/theorem had been verified. Am I incorrect about that? (If the explanation is complicated, please don't feel obligated to go into complete detail. A one-word answer will tell me all I probably <i>need</i> to know. Any further explanation would just be to satisfy my beginner's curiosity)</div>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"><br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
EXPLANATION/DETAIL:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
>From what I've read in the documentation, structured Isar proofs are<br>
</blockquote>
preferred over apply-style proofs in every case except for<br>
prototyping/experimentation.<br>
</blockquote>
<br></div>
Unstructured proof scripts (now called "apply style) and structured Isar proofs are historically, technically, conceptually somehow related, although in retrospect this is somehow accidental.  The Isabelle/Isar system was made in a way to include the old script style as "guest" to the new approach.  This worked so smoothly that people sometimes think that Isar is still about "proof scripts", but it is actually about "proof documents".<br>


<br>
Moving back and forth between the two styles works for many Isabelle experts after some practice, although my impression in recent years is that it would be better to teach people just one style from the start, and not pretend that one is a prerequisite to the other.  (E.g. in Isabelle2013 'by' no longer needs to be broken up into 1-2 'apply' to diagnose its failure.)<br>


<br>
There is a long story behind that, of how the system presents it by default and how the manuals are written.  And it is getting more and more off-topic for isabelle-dev, which is about the development process, and exploring / testing intermediate Isabelle snapshots between official releases -- i.e. the everyday struggles with ongoing changes, not a relaxed discussion about the big picture.</blockquote>

<div>I apologize if I brought up an already over-discussed topic. If I have any further questions about "proof scripts" vs "proof documents", I'll begin in the isabelle-users mailing list.</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<span class="HOEnZb"><font color="#888888"><br>
<br>
<br>
        Makarius<br>
</font></span></blockquote></div><br></div></div>