src/FOL/FOL.thy
changeset 23154 5126551e378b
parent 22139 539a63b98f76
child 24097 86734ba03ca2
equal deleted inserted replaced
23153:3cc4a80c4d30 23154:5126551e378b
     5 
     5 
     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 ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    10 uses
       
    11   ("cladata.ML")
       
    12   ("blastdata.ML")
       
    13   ("simpdata.ML")
    11 begin
    14 begin
    12 
    15 
    13 
    16 
    14 subsection {* The classical axiom *}
    17 subsection {* The classical axiom *}
    15 
    18