Re: [isabelle] Isabelle style guide



Very nice styleguide! It very much matches what I am trying to do in my
proofs, too. Except for the apply-indentation scheme, where I use
somewhat different:
	
	If a method produces n new subgoals, the next apply-steps will be
indented one level, and grouped into n blocks by blank lines, where each
block solves one of the subgoals:


  apply (intro conjI)    // produces 3 subgoals
    apply auto []        // Solves first one

    apply (cases l)      // Solve 2nd one
      apply clarsimp       // Solve Nil-case
      apply force

      apply auto []        // Solve Cons-case

    apply force          // Solve 3rd subgoal
  done


--
  Peter


On Sa, 2015-05-23 at 10:14 +0000, Gerwin Klein wrote:
> Updating lots of proofs to Isabelle2015-RCx and discussions about submission rules for the AFP inspired me to write up guidelines that may be of more widespread use and interest:
> 
> http://proofcraft.org/blog/isabelle-style.html
> 
> Thereâs more to come. Feedback welcome.
> 
> Enjoy!
> Gerwin
> 
> 
> ________________________________
> 
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.