Re: [isabelle] How do I do stone age interaction?

On 27/11/10 11:25, Makarius 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.
>     Makarius
Not so - my own TPHOLs papers in 2002, 2007 and 2009, plus my track B
presentations in 2002 and 2007, and several other papers presented
elsewhere, all describe work proving things in different areas, all
using Isabelle, none using Isar.


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