# HG changeset patch
# User wenzelm
# Date 1005342632 -3600
# Node ID 219e543496a3584b047ebaa5704bec667c0707ad
# Parent  34f72eb7d2db023572770a3d8821105f8a806d11
theorems case_split = case_split_thm [case_names True False, cases type: o];

diff -r 34f72eb7d2db -r 219e543496a3 src/FOL/FOL.thy
--- 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