# HG changeset patch
# User paulson
# Date 1021063878 -7200
# Node ID 3c6400ad94309dfd58e03def8bf4e4094ffb9b61
# Parent  bf37a3049251500fa92d5d17404d66f0480d0c18
now-obsolete ML files

diff -r bf37a3049251 -r 3c6400ad9430 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Fri May 10 22:50:08 2002 +0200
+++ b/src/ZF/IsaMakefile	Fri May 10 22:51:18 2002 +0200
@@ -28,11 +28,11 @@
 FOL:
 	@cd $(SRC)/FOL; $(ISATOOL) make FOL
 
-$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy ArithSimp.ML	\
+$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.ML Arith.thy ArithSimp.ML	\
   ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy		\
-  CardinalArith.ML CardinalArith.thy Cardinal_AC.ML Cardinal_AC.thy	\
+  CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \
   Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy Finite.ML Finite.thy	\
-  Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy InfDatatype.ML	\
+  Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy 	\
   InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML	\
   Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
   Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\
@@ -46,7 +46,7 @@
   Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
   Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
   Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
-  WF.thy ZF.ML ZF.thy Zorn.ML Zorn.thy arith_data.ML domrange.ML	\
+  WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML domrange.ML	\
   domrange.thy equalities.ML equalities.thy func.ML func.thy		\
   ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
   subset.ML subset.thy thy_syntax.ML upair.ML upair.thy