src/FOL/FOL.thy
changeset 16417 9bc16273c2d4
parent 15481 fc075ae929e4
child 18456 8cc35e95450a
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     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 files ("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")
    11       ("eqrule_FOL_data.ML")
    12       ("~~/src/Provers/eqsubst.ML")
    12       ("~~/src/Provers/eqsubst.ML")
    13 begin  
    13 begin  
    14 
    14 
    15 
    15