src/FOL/FOL.thy
changeset 8471 36446bf42b16
parent 7355 4c43090659ca
child 8643 331f0c75e3dc
equal deleted inserted replaced
8470:f06fc940c61c 8471:36446bf42b16
     4 
     4 
     5 axioms
     5 axioms
     6   classical: "(~P ==> P) ==> P"
     6   classical: "(~P ==> P) ==> P"
     7 
     7 
     8 use "FOL_lemmas1.ML"
     8 use "FOL_lemmas1.ML"
     9 use "cladata.ML"	setup Cla.setup setup clasetup
     9 use "cladata.ML"        setup Cla.setup setup clasetup
    10 use "blastdata.ML"	setup Blast.setup
    10 use "blastdata.ML"      setup Blast.setup
    11 use "FOL_lemmas2.ML"
    11 use "FOL_lemmas2.ML"
    12 use "simpdata.ML"	setup simpsetup setup Clasimp.setup
    12 use "simpdata.ML"       setup simpsetup
       
    13                         setup "Simplifier.method_setup Splitter.split_modifiers"
       
    14                         setup Splitter.setup setup Clasimp.setup
    13 
    15 
    14 end
    16 end