1.1 --- a/src/HOL/IsaMakefile Wed Apr 29 11:37:58 1998 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed Apr 29 11:38:52 1998 +0200
1.3 @@ -43,14 +43,14 @@
1.4 Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.ML \
1.5 Inductive.thy Lfp.ML Lfp.thy List.ML List.thy Map.ML Map.thy Nat.ML \
1.6 Nat.thy NatDef.ML NatDef.thy Option.ML Option.thy Ord.ML Ord.thy \
1.7 - Power.ML Power.thy Prod.ML Prod.thy ROOT.ML RelPow.ML RelPow.thy \
1.8 - Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy Sum.ML \
1.9 - Sum.thy Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy \
1.10 - WF.ML WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML \
1.11 - cladata.ML datatype.ML equalities.ML equalities.thy hologic.ML \
1.12 - ind_syntax.ML indrule.ML indrule.thy intr_elim.ML intr_elim.thy \
1.13 - mono.ML mono.thy record.ML simpdata.ML subset.ML subset.thy \
1.14 - thy_data.ML thy_syntax.ML typedef.ML
1.15 + Power.ML Power.thy Prod.ML Prod.thy Record.thy ROOT.ML RelPow.ML \
1.16 + RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
1.17 + Sum.ML Sum.thy Tools/record_package.ML Tools/typedef_package.ML \
1.18 + Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \
1.19 + WF.thy WF_Rel.ML WF_Rel.thy add_ind_def.ML arith_data.ML cladata.ML \
1.20 + datatype.ML equalities.ML equalities.thy hologic.ML ind_syntax.ML \
1.21 + indrule.ML indrule.thy intr_elim.ML intr_elim.thy mono.ML mono.thy \
1.22 + simpdata.ML subset.ML subset.thy thy_data.ML thy_syntax.ML
1.23 @$(ISATOOL) usedir -b $(OUT)/Pure HOL
1.24
1.25
2.1 --- a/src/HOL/ROOT.ML Wed Apr 29 11:37:58 1998 +0200
2.2 +++ b/src/HOL/ROOT.ML Wed Apr 29 11:38:52 1998 +0200
2.3 @@ -35,11 +35,12 @@
2.4
2.5 use_thy "Ord";
2.6 use_thy "subset";
2.7 -use "typedef.ML";
2.8 +use "Tools/typedef_package.ML";
2.9 use_thy "Sum";
2.10 use_thy "Gfp";
2.11
2.12 -use "record.ML";
2.13 +use "Tools/record_package.ML";
2.14 +use_thy "Record";
2.15
2.16 use "datatype.ML";
2.17 use_thy "Arith";