On Tue, Jul 30, 2013 at 3:42 PM, Lawrence Paulson <[email protected]> wrote:
> This could be a valuable service, especially for long lists of applys. > Thank you for the encouragement! I'm glad to see you agree. > (A proof like "by (induct n) auto" should be left alone.) > Understood. If I come across proofs comprising only two `apply`s, should I tweak them to use the briefer `by method1 method2` form? Or would that be considered a pedantic waste of time? > > Do ask an experienced user to examine your early attempts for beginner's > mistakes, like labelling all intermediate results. > Happy to oblige. > > Larry > > On 30 Jul 2013, at 18:40, Josh Tilles <[email protected]> wrote: > > 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? > > EXPLANATION/DETAIL: > 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) > 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. > *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. > > --Josh > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > >
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
