src/HOL/PreList.thy
changeset 10261 bb2f1e859177
parent 10212 33fe2d701ddd
child 10519 ade64af4c57c
--- 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