src/FOL/FOL.thy
author wenzelm
Fri Mar 31 22:22:23 2000 +0200 (2000-03-31 ago)
changeset 8643 331f0c75e3dc
parent 8471 36446bf42b16
child 9487 7e377f912629
permissions -rw-r--r--
added cong atts;
     1 
     2 theory FOL = IFOL
     3 files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"):
     4 
     5 axioms
     6   classical: "(~P ==> P) ==> P"
     7 
     8 use "FOL_lemmas1.ML"
     9 use "cladata.ML"        setup Cla.setup setup clasetup
    10 use "blastdata.ML"      setup Blast.setup
    11 use "FOL_lemmas2.ML"
    12 use "simpdata.ML"       setup simpsetup setup cong_attrib_setup
    13                         setup "Simplifier.method_setup Splitter.split_modifiers"
    14                         setup Splitter.setup setup Clasimp.setup
    15 
    16 end