src/FOL/FOL.thy
changeset 12127 219e543496a3
parent 11988 8340fb172607
child 12160 a5cf3ea0685d
equal deleted inserted replaced
12126:34f72eb7d2db 12127:219e543496a3
    18 
    18 
    19 
    19 
    20 subsection {* Lemmas and proof tools *}
    20 subsection {* Lemmas and proof tools *}
    21 
    21 
    22 use "FOL_lemmas1.ML"
    22 use "FOL_lemmas1.ML"
    23 theorems case_split = case_split_thm [case_names True False]
    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 
    28