Re: [isabelle] Theorem-proving for a Bayesian model compiler

On Thu, 17 Mar 2011, Timothy McKenzie wrote:

And if you don't know exactly what you want to prove before you've proven it, you can make the statement of the lemma almost arbitrary until you've figured out what you want to prove, and then go back and change it.

Maybe the recent 'notepad' is also of some interest here, it nicely shows how Isabelle/Isar works without goal states getting in the way:


  fix x y z :: 'a
  assume "x = y"
  also assume "... = z"
  finally have "x = z" .



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