src/FOL/FOL.thy
changeset 18595 a52907967bae
parent 18591 04b9f2bf5a48
child 18816 aebd7f315b92
equal deleted inserted replaced
18594:e0d509b1df1d 18595:a52907967bae
     6 header {* Classical first-order logic *}
     6 header {* Classical first-order logic *}
     7 
     7 
     8 theory FOL
     8 theory FOL
     9 imports IFOL
     9 imports IFOL
    10 uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    10 uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    11       ("eqrule_FOL_data.ML")
       
    12       ("~~/src/Provers/eqsubst.ML")
       
    13 begin
    11 begin
    14 
    12 
    15 
    13 
    16 subsection {* The classical axiom *}
    14 subsection {* The classical axiom *}
    17 
    15 
    43 use "simpdata.ML"
    41 use "simpdata.ML"
    44 setup simpsetup
    42 setup simpsetup
    45 setup "Simplifier.method_setup Splitter.split_modifiers"
    43 setup "Simplifier.method_setup Splitter.split_modifiers"
    46 setup Splitter.setup
    44 setup Splitter.setup
    47 setup Clasimp.setup
    45 setup Clasimp.setup
    48 
       
    49 
       
    50 subsection {* Lucas Dixon's eqstep tactic *}
       
    51 
       
    52 use "~~/src/Provers/eqsubst.ML";
       
    53 use "eqrule_FOL_data.ML";
       
    54 
       
    55 setup EqSubst.setup
    46 setup EqSubst.setup
    56 
    47 
    57 
    48 
    58 subsection {* Other simple lemmas *}
    49 subsection {* Other simple lemmas *}
    59 
    50