src/HOL/PreList.thy
changeset 9066 b1e874e38dab
parent 8862 78643f8449c6
child 9619 6125cc9efc18
--- a/src/HOL/PreList.thy	Wed Jun 14 17:47:18 2000 +0200
+++ b/src/HOL/PreList.thy	Wed Jun 14 17:59:53 2000 +0200
@@ -11,4 +11,6 @@
   Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
   SVC_Oracle:
 
+theorems [cases type: bool] = case_split
+
 end