Re: [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)




In attempting to run Isabelle 2008, I get

jeremy at stiletto:~/isabelle/2008/gen$ isabelle
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=204800K,ib=40960K,ip=100%,mb=45056K,mp=20%)
Mapping /home/users/jeremy/isabelle/heaps/Isabelle2008/polyml-4.1.4_x86-linux/HOL
Mapping /home/users/jeremy/Isabelle2008/../polyml/x86-linux/ML_dbase
Poly/ML 4.2.0 Release
>  Goal "X";
Exception- ERROR "Unknown context" raised

In Isabelle 2007 (and prior) this works fine

jeremy at stiletto:~/isabelle/2007$ is07
Poly/ML RTS version I386-4.1.4 (14:18:30 Nov 14 2005)
Copyright (c) 2002-5 CUTS and contributors.
Running with heap parameters (h=512000K,ib=102400K,ip=100%,mb=106496K,mp=20%)
Mapping /home/users/jeremy/Isabelle2007/heaps/polyml-4.1.4_x86-linux/HOL
Mapping /home/users/jeremy/Isabelle2007/../polyml/x86-linux/ML_dbase
Poly/ML 4.2.0 Release
> Goal ;
val it = fn : string -> Thm.thm list
> Goal "X";
### Legacy feature: old goal command
Level 0 (1 subgoal)
X
1. X
val it = [] : Thm.thm list

What has happened here?

Jeremy






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