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:

notepad
begin

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

end


	Makarius





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