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;
wenzelm@4093
     1
wenzelm@7355
     2
theory FOL = IFOL
wenzelm@7355
     3
files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"):
wenzelm@4093
     4
wenzelm@7355
     5
axioms
wenzelm@7355
     6
  classical: "(~P ==> P) ==> P"
wenzelm@4093
     7
wenzelm@7355
     8
use "FOL_lemmas1.ML"
wenzelm@8471
     9
use "cladata.ML"        setup Cla.setup setup clasetup
wenzelm@8471
    10
use "blastdata.ML"      setup Blast.setup
wenzelm@7355
    11
use "FOL_lemmas2.ML"
wenzelm@8643
    12
use "simpdata.ML"       setup simpsetup setup cong_attrib_setup
wenzelm@8471
    13
                        setup "Simplifier.method_setup Splitter.split_modifiers"
wenzelm@8471
    14
                        setup Splitter.setup setup Clasimp.setup
wenzelm@4093
    15
wenzelm@4854
    16
end