<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">This could be a valuable service, especially for long lists of applys. (A proof like "by (induct n) auto" should be left alone.)<div><br></div><div>Do ask an experienced user to examine your early attempts for beginner's mistakes, like labelling all intermediate results.</div><div><br><div apple-content-edited="true">
<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 11px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0; ">Larry</span>
</div>
<br><div><div>On 30 Jul 2013, at 18:40, Josh Tilles <<a href="mailto:merelyapseudonym@gmail.com">merelyapseudonym@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr"><div>QUESTION STATED BRIEFLY:<br></div>If I convert existing proofs in <span style="font-family:courier new,monospace">src/HOL/**.thy</span> from apply-style to Isar-style, would those changes be welcome in the main repository?<br>
<div><br>EXPLANATION/DETAIL:<br>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)<br>
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.<br>*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.<br>
<br>--Josh<br></div></div>
_______________________________________________<br>isabelle-dev mailing list<br><a href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br></blockquote></div><br></div></body></html>