# HG changeset patch
# User wenzelm
# Date 893842732 -7200
# Node ID 3abfe2093aa082c4afbc5d7bc83cecd2d068d59e
# Parent  d29776582f8ccff1b20f7b4ea089f21f47bb27b5
removed typedef.ML, record.ML;
added Tools/typedef_package.ML, Tools/record_package.ML, Record.thy;

diff -r d29776582f8c -r 3abfe2093aa0 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Apr 29 11:37:58 1998 +0200
+++ b/src/HOL/IsaMakefile	Wed Apr 29 11:38:52 1998 +0200
@@ -43,14 +43,14 @@
   Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.ML \
   Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
   Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
-  Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML RelPow.thy \
-  Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy Sum.ML \
-  Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy \
-  WF.ML WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML \
-  cladata.ML datatype.ML equalities.ML equalities.thy hologic.ML \
-  ind_syntax.ML indrule.ML indrule.thy intr_elim.ML intr_elim.thy \
-  mono.ML mono.thy record.ML simpdata.ML subset.ML subset.thy \
-  thy_data.ML thy_syntax.ML typedef.ML
+  Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \
+  RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
+  Sum.ML Sum.thy Tools/record_package.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 add_ind_def.ML arith_data.ML cladata.ML \
+  datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \
+  indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \
+  simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
 
diff -r d29776582f8c -r 3abfe2093aa0 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Apr 29 11:37:58 1998 +0200
+++ b/src/HOL/ROOT.ML	Wed Apr 29 11:38:52 1998 +0200
@@ -35,11 +35,12 @@
 
 use_thy "Ord";
 use_thy "subset";
-use "typedef.ML";
+use "Tools/typedef_package.ML";
 use_thy "Sum";
 use_thy "Gfp";
 
-use "record.ML";
+use "Tools/record_package.ML";
+use_thy "Record";
 
 use "datatype.ML";
 use_thy "Arith";