Email Gateway (Aug 17 2022 at 14:49): Email Gateway (Aug 17 2022 at 14:49):From: Hannes Verlinde <Hannes.Verlinde@UGent.be>
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
Email Gateway (Aug 17 2022 at 14:49):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 12:27 UTC