changeset 12127 | 219e543496a3 |
parent 11988 | 8340fb172607 |
child 12160 | a5cf3ea0685d |
--- a/src/FOL/FOL.thy Fri Nov 09 10:26:16 2001 +0100 +++ b/src/FOL/FOL.thy Fri Nov 09 22:50:32 2001 +0100 @@ -20,7 +20,7 @@ subsection {* Lemmas and proof tools *} use "FOL_lemmas1.ML" -theorems case_split = case_split_thm [case_names True False] +theorems case_split = case_split_thm [case_names True False, cases type: o] use "cladata.ML" setup Cla.setup