tuned declarations;
authorwenzelm
Wed Oct 18 23:40:17 2000 +0200 (2000-10-18)
changeset 10261bb2f1e859177
parent 10260 6c31c8bb78e8
child 10262 3c43e8086cba
tuned declarations;
src/HOL/Main.thy
src/HOL/PreList.thy
     1.1 --- a/src/HOL/Main.thy	Wed Oct 18 23:39:49 2000 +0200
     1.2 +++ b/src/HOL/Main.thy	Wed Oct 18 23:40:17 2000 +0200
     1.3 @@ -4,8 +4,8 @@
     1.4  
     1.5  theory Main = Map + String:
     1.6  
     1.7 -(*actually belongs to theory List*)
     1.8 -lemmas [mono] = lists_mono
     1.9 -lemmas [recdef_cong] = map_cong
    1.10 +(*belongs to theory List*)
    1.11 +declare lists_mono [mono]
    1.12 +declare map_cong [recdef_cong]
    1.13  
    1.14  end
     2.1 --- a/src/HOL/PreList.thy	Wed Oct 18 23:39:49 2000 +0200
     2.2 +++ b/src/HOL/PreList.thy	Wed Oct 18 23:40:17 2000 +0200
     2.3 @@ -9,8 +9,12 @@
     2.4  
     2.5  theory PreList =
     2.6    Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
     2.7 -  Relation_Power + Calculation + SVC_Oracle + While:
     2.8 +  Relation_Power + Calculation + SVC_Oracle:
     2.9  
    2.10 -theorems [cases type: bool] = case_split
    2.11 +(*belongs to theory HOL*)
    2.12 +declare case_split [cases type: bool]
    2.13 +
    2.14 +(*belongs to theory Wellfounded_Recursion*)
    2.15 +declare wf_induct [induct set: wf]
    2.16  
    2.17  end