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