src/HOL/IsaMakefile
changeset 14430 5cb24165a2e1
parent 14429 0fce2d8bce0f
child 14432 b02de2918c59
--- a/src/HOL/IsaMakefile	Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 04 12:06:07 2004 +0100
@@ -87,9 +87,8 @@
   HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
   Integ/cooper_dec.ML Integ/cooper_proof.ML \
   Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
-  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy \
-  Integ/int_arith1.ML \
-  Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
+  Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
+  Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
   Nat.thy NatArith.ML NatArith.thy Numeral.thy \
@@ -143,7 +142,7 @@
   Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
   Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
   Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
-  Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
+  Hyperreal/EvenOdd.thy\
   Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
   Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
   Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\