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



Thanks for you replies everyone.  It sounds like I need to take a look at
Isar in Isabelle2009 then.  I'll also be looking at Isabelle98.

on 6/12/10 4:20 PM, Makarius <makarius at sketis.net> wrote:

> My understanding was that you want to see the "proof technologies" behind
> the Isabelle system :-)

Aha I see! :)

> Isabelle2005 is a rock solid distribution, but also a particularly
> confusing one due to many old layers being still in there.  This is why I
> mentioned the more basic Isabelle98, although it lacks the main concepts
> of contempory Isabelle.

I'll be taking a look at Isabelle98 then.  Basic stone age is what I need.
Thanks.

> Anyway, when I want to understand Linux, I also stay within the normal
> user space, instead of booting into single user mode with the init process
> running a single instance of bash.

Therein lies the difference between us.  To understand HOL4 I first look at
HOL90 in detail!

> The old HOL manual has hardly ever been maintained in the past 10 years.
> The term syntax is defined in library space in the context.  The
> print_syntax command will tell you some aspects of it.

In which document can I find a comprehensive description of the (presumably
ASCII) lex (any version of Isabelle will do for starters)?   And does the
lex vary between logics?

Mark.





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