Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
On Wed, 8 Oct 2008, Jeremy Dawson wrote:
> In attempting to run Isabelle 2008, I get
> > Goal "X";
> Exception- ERROR "Unknown context" raised
> In Isabelle 2007 (and prior) this works fine
> > Goal "X";
> ### Legacy feature: old goal command
> Level 0 (1 subgoal)
> 1. X
> val it =  : Thm.thm list
> What has happened here?
Even in Isabelle2007 it clearly says that the old ML Goal command is a
legacy feature -- few contemporary Isabelle users will remember that it
Legacy features just disappear at some point. In Isabelle2008 the ML
function still happens to be around, but does not work without a proper
context -- almost everything in Isabelle needs one.
In the forthcoming Isabelle release even plain ML bindings already require
a context -- we will have a purely functional ML toplevel that works
seamlessly with undo and multithreading.
There are two ways to issue ML stuff *with* a context:
* Either: use the 'ML' command within the Isar toplevel, usually within
Proof General. This is the regular, preferred way.
* Or: startup a raw tty Isar loop, e.g. using "isatool tty", enter a
theory, exit, poke around in ML, re-enter Isar:
$ isatool tty -l HOL
> theory A imports Maib begin
ML> Isar.loop ()
This scheme is useful for debugging in rare situations, e.g. when
there are problems in conjunction with the Isar toplevel itself.
This archive was generated by a fusion of
Pipermail (Mailman edition) and