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