1.1 --- a/src/HOL/IsaMakefile	Thu Mar 16 00:33:46 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 16 00:35:27 2000 +0100
     1.3 @@ -52,9 +52,9 @@
     1.4    Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \
     1.5    Integ/NatBin.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
     1.6    Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
     1.7 -  Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy \
     1.8 -  ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML \
     1.9 -  Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    1.10 +  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
    1.11 +  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
    1.12 +  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
    1.13    SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
    1.14    Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
    1.15    Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
    1.16 @@ -62,7 +62,7 @@
    1.17    Tools/numeral_syntax.ML Tools/primrec_package.ML \
    1.18    Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
    1.19    Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
    1.20 -  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
    1.21 +  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML  \
    1.22    cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
    1.23    simpdata.ML subset.ML subset.thy thy_syntax.ML
    1.24  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL

     2.1 --- a/src/HOL/List.thy	Thu Mar 16 00:33:46 2000 +0100
     2.2 +++ b/src/HOL/List.thy	Thu Mar 16 00:35:27 2000 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  The datatype of finite lists.
     2.5  *)
     2.6  
     2.7 -List = Datatype + WF_Rel + NatBin +
     2.8 +List = PreList +
     2.9  
    2.10  datatype 'a list = Nil ("[]") | Cons 'a ('a list) (infixr "#" 65)
    2.11  

     3.1 --- a/src/HOL/Main.thy	Thu Mar 16 00:33:46 2000 +0100
     3.2 +++ b/src/HOL/Main.thy	Thu Mar 16 00:35:27 2000 +0100
     3.3 @@ -1,5 +1,1 @@
     3.4 -
     3.5 -(*theory Main includes everything*)
     3.6 -
     3.7 -Main = NatBin + Map + Recdef + Record + RelPow + Sexp + String + Calculation +
     3.8 -       SVC_Oracle
     3.9 +Main = Map + String             (*theory Main includes everything*)

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/PreList.thy	Thu Mar 16 00:35:27 2000 +0100
     4.3 @@ -0,0 +1,5 @@
     4.4 +
     4.5 +theory PreList =
     4.6 +  Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation + SVC_Oracle:
     4.7 +
     4.8 +end