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.

Jeremy






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