added HOL/PreLIst.thy;

--- a/src/HOL/IsaMakefile	Thu Mar 16 00:33:46 2000 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 16 00:35:27 2000 +0100
@@ -52,9 +52,9 @@
   Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \
   Integ/NatBin.thy Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
   Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
-  Option.thy Ord.ML Ord.thy Power.ML Power.thy Prod.ML Prod.thy \
-  ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML \
-  Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
+  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
+  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
+  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
   SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
   Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
@@ -62,7 +62,7 @@
   Tools/numeral_syntax.ML Tools/primrec_package.ML \
   Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
   Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
-  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
+  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML  \
   cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
   simpdata.ML subset.ML subset.thy thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL

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

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

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