# HG changeset patch
# User wenzelm
# Date 971905217 -7200
# Node ID bb2f1e859177fa8d66c39f2ca68f57be9d8335b2
# Parent  6c31c8bb78e86cec2362800095aa4b1b9a9ac846
tuned declarations;

diff -r 6c31c8bb78e8 -r bb2f1e859177 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Oct 18 23:39:49 2000 +0200
+++ b/src/HOL/Main.thy	Wed Oct 18 23:40:17 2000 +0200
@@ -4,8 +4,8 @@
 
 theory Main = Map + String:
 
-(*actually belongs to theory List*)
-lemmas [mono] = lists_mono
-lemmas [recdef_cong] = map_cong
+(*belongs to theory List*)
+declare lists_mono [mono]
+declare map_cong [recdef_cong]
 
 end
diff -r 6c31c8bb78e8 -r bb2f1e859177 src/HOL/PreList.thy
--- 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