src/FOL/FOL.thy
author wenzelm
Sat, 01 Jul 2000 19:55:22 +0200
changeset 9230 17ae63f82ad8
parent 8643 331f0c75e3dc
child 9487 7e377f912629
permissions -rw-r--r--
GPLed;


theory FOL = IFOL
files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"):

axioms
  classical: "(~P ==> P) ==> P"

use "FOL_lemmas1.ML"
use "cladata.ML"        setup Cla.setup setup clasetup
use "blastdata.ML"      setup Blast.setup
use "FOL_lemmas2.ML"
use "simpdata.ML"       setup simpsetup setup cong_attrib_setup
                        setup "Simplifier.method_setup Splitter.split_modifiers"
                        setup Splitter.setup setup Clasimp.setup

end