# 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";