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.
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and