--- a/src/HOL/PreList.thy Wed Oct 18 23:39:49 2000 +0200
+++ b/src/HOL/PreList.thy Wed Oct 18 23:40:17 2000 +0200
@@ -9,8 +9,12 @@
theory PreList =
Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
- Relation_Power + Calculation + SVC_Oracle + While:
+ Relation_Power + Calculation + SVC_Oracle:
-theorems [cases type: bool] = case_split
+(*belongs to theory HOL*)
+declare case_split [cases type: bool]
+
+(*belongs to theory Wellfounded_Recursion*)
+declare wf_induct [induct set: wf]
end