*To*: Timothy McKenzie <tjm1983 at gmail.com>*Subject*: Re: [isabelle] Theorem-proving for a Bayesian model compiler*From*: Makarius <makarius at sketis.net>*Date*: Thu, 17 Mar 2011 10:46:52 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201103171252.29679.tjm1983@gmail.com>*References*: <8AC639F1-C740-46CC-9F0C-C4093B16B51C@ksvanhorn.com> <201103171252.29679.tjm1983@gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Thu, 17 Mar 2011, Timothy McKenzie wrote:

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

notepad begin fix x y z :: 'a assume "x = y" also assume "... = z" finally have "x = z" . end Makarius

**References**:**[isabelle] Theorem-proving for a Bayesian model compiler***From:*Kevin Van Horn

**Re: [isabelle] Theorem-proving for a Bayesian model compiler***From:*Timothy McKenzie

- Previous by Date: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Next by Date: [isabelle] Post-doc position: Timed systems
- Previous by Thread: Re: [isabelle] Theorem-proving for a Bayesian model compiler
- Next by Thread: [isabelle] How do I make notation work only on the constant instead of on the type as well?
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list