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
Exception- ERROR "Unknown context" raised
In Isabelle 2007 (and prior) this works fine
### Legacy feature: old goal command
Level 0 (1 subgoal)
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
The "old" ML Goal command was introduced in October 1998!! It was said
to _improve_ upon the old "goal" command, which _did_ require a context.
Incidentally, the prove_goal command - which was purely functional, and
the "goal" command, which required specifying the context, were left
unchanged, even though the developers then thought that non purely
functional code was preferable. Those users who preferred purely
functional ML code were given the option to continue using it. They
were not compelled to go to the inconvenience of changing all their code
just because the developers then had a different preference.
If few contemporary Isabelle users will remember that the Goal command
existed, that means that, of those who used Isabelle when the Goal
command was in common use, most are no longer Isabelle users. This may
well be true, I wouldn't be surprised. But if few people can survive
using Isabelle for more than a few years, that is not a great
recommendation for it.
And what of the proofs those users did using Isabelle? Pen and paper
proofs, once published, will still be in libraries for a hundred years.
An Isabelle proof, using "Goal", will, in approach reflected in your
email and other, have had a useful life of only a few years.
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.
Does this mean that all the functions involving an implicit context will
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.
eg, Simp_tac, simpset, etc ? My code is full of these.
I notice that the_context() has disappeared from Isabelle2008.
Thanks. Incidentally, I notice that the_context() has disappeared from
Once one has created the context by entering Isar and exiting it again,
how does one get hold of it?
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