src/FOL/FOL.thy
changeset 12367 1cee8a0db392
parent 12303 67ca723a02dd
child 13550 5a176b8dda84
equal deleted inserted replaced
12366:f0fd3c4f2f49 12367:1cee8a0db392
    23 theorems case_split = case_split_thm [case_names True False, cases type: o]
    23 theorems case_split = case_split_thm [case_names True False, cases type: o]
    24 
    24 
    25 use "cladata.ML"
    25 use "cladata.ML"
    26 setup Cla.setup
    26 setup Cla.setup
    27 setup clasetup
    27 setup clasetup
    28 
       
    29 declare disjI1 [elim?]  disjI2 [elim?]
       
    30 
    28 
    31 use "blastdata.ML"
    29 use "blastdata.ML"
    32 setup Blast.setup
    30 setup Blast.setup
    33 use "FOL_lemmas2.ML"
    31 use "FOL_lemmas2.ML"
    34 
    32