Re: [isabelle] Setting up the Simplifier in Isabelle2005



On Thu, 29 Jun 2006, Hannes Verlinde wrote:

> I'm currently updating my theory files for use with the latest Isabelle
> distribution, but I'm having some trouble with setting up the simplifier.

> use "~~/src/Pure/simplifier.ML"

> But the line "setup simpsetup" now fails with the error message
> "Uninitialized theory data "Pure/simpset"".

Things should work out as expected, if you do not load 
"~~/src/Pure/simplifier.ML" a second time.  See also the Simplifier setup 
in src/FOL/FOL.thy or src/HOL/HOL.thy for example.


	Makarius





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