[isabelle] Setting up the Simplifier in Isabelle2005



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.
After reading the NEWS file, I have changed the following lines from:

 

use “~~/src/Provers/simplifier.ML”

setup “Simplifier.setup”

use “simpdata.ML”

setup simpsetup

setup “Simplifier.method_setup []”

 

to:

 

use “~~/src/Pure/simplifier.ML”

use “simpdata.ML”

setup simpsetup

setup “Simplifier.method_setup []”

 

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

Thanks in advance for any help or advice.

 

Hannes Verlinde

Ghent University


--
No virus found in this outgoing message.
Checked by AVG Free Edition.
Version: 7.1.394 / Virus Database: 268.9.6/378 - Release Date: 28/06/2006



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