--- 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