fixed deps;
authorwenzelm
Thu Aug 17 10:33:37 2000 +0200 (2000-08-17)
changeset 96196125cc9efc18
parent 9618 ff8238561394
child 9620 1adf6d761c97
fixed deps;
src/HOL/Main.thy
src/HOL/PreList.thy
     1.1 --- a/src/HOL/Main.thy	Thu Aug 17 10:33:13 2000 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu Aug 17 10:33:37 2000 +0200
     1.3 @@ -1,1 +1,5 @@
     1.4 -Main = While + Map + String             (*theory Main includes everything*)
     1.5 +
     1.6 +(*theory Main includes everything; note that theory
     1.7 +  PreList already includes most HOL theories*)
     1.8 +
     1.9 +Main = Map + String
     2.1 --- a/src/HOL/PreList.thy	Thu Aug 17 10:33:13 2000 +0200
     2.2 +++ b/src/HOL/PreList.thy	Thu Aug 17 10:33:37 2000 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  
     2.5  theory PreList =
     2.6    Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation + 
     2.7 -  SVC_Oracle:
     2.8 +  SVC_Oracle + While:
     2.9  
    2.10  theorems [cases type: bool] = case_split
    2.11