Re: [isabelle] How do I do stone age interaction?
Probably you should look at the papers at http://www.cl.cam.ac.uk/~lp15/papers/isabelle.html
Look particularly at the papers under the tab “of historical interest".
On 28 Nov 2010, at 12:58, <mark at proof-technologies.com> wrote:
> on 27/11/10 11:25 AM, Makarius <makarius at sketis.net> wrote:
>> In order to be productive with Isabelle/ML you should build up your
>> context in Isar source notation and the experiment with it via small ML
>> snippets. What is your application anyway? Serious use of Isabelle
>> outside the Isar system infrastructure is hard to imagine.
> Unlike other users, I'm not aiming to use Isabelle for performing proofs as
> such. Rather I'm looking to gain a deep understanding of how Isabelle
> works. But thanks for the Isar example for Socrates, which will help me
> understand Isar.
> on 27/11/10 11:55 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>> You might consider downloading an older version from here:
>> Until around 2005, ML level interaction was still supported.
> Thanks. I've got Isabelle 2005 with HOL up and running now (curiously, this
> required a handful of changes to the Isabelle ML source code to get it
> through what purports to be Poly/ML 4.1.4). But how do I enter HOL term and
> type quotations into the session? And what are the HOL term and type
> constructor functions?
This archive was generated by a fusion of
Pipermail (Mailman edition) and