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
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