--- a/src/HOL/IsaMakefile Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 24 13:03:20 1998 +0200
@@ -39,19 +39,23 @@
$(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \
$(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \
$(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \
- Arith.ML Arith.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
+ Arith.ML Arith.thy Datatype.thy \
+ Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \
Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy Inductive.thy Integ/Bin.ML \
Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/Integ.ML \
Integ/Integ.thy Lfp.ML Lfp.thy List.ML List.thy Main.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 Recdef.thy Record.thy RelPow.ML \
RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
- String.ML String.thy Sum.ML Sum.thy Tools/inductive_package.ML Tools/record_package.ML \
+ String.ML String.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 \
+ Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
- WF_Rel.thy arith_data.ML cladata.ML datatype.ML equalities.ML \
+ WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
- subset.thy thy_data.ML thy_syntax.ML
+ subset.thy thy_syntax.ML
@$(ISATOOL) usedir -b $(OUT)/Pure HOL