--- a/src/HOL/IsaMakefile Sun Oct 01 18:29:23 2006 +0200
+++ b/src/HOL/IsaMakefile Sun Oct 01 18:29:25 2006 +0200
@@ -88,7 +88,7 @@
Datatype_Universe.thy Divides.thy \
Equiv_Relations.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
FixedPoint.thy Fun.thy HOL.ML HOL.thy Hilbert_Choice.thy Inductive.thy \
- Infinite_Set.thy Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy \
+ Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy \
Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Numeral.thy \
Integ/Parity.thy Integ/Presburger.thy Integ/cooper_dec.ML \
Integ/cooper_proof.ML Integ/reflected_presburger.ML \
@@ -181,7 +181,8 @@
Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy \
Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy \
- Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex
+ Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex \
+ Library/Infinite_Set.thy
@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
@@ -203,7 +204,7 @@
$(LOG)/HOL-Library.gz: $(OUT)/HOL \
Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
- Library/MLString.thy \
+ Library/MLString.thy Library/Infinite_Set.thy \
Library/FuncSet.thy Library/Library.thy \
Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
@@ -342,7 +343,7 @@
NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
NumberTheory/Finite2.thy NumberTheory/Int2.thy NumberTheory/EvenOdd.thy\
NumberTheory/Residues.thy NumberTheory/Euler.thy NumberTheory/Gauss.thy\
- NumberTheory/Quadratic_Reciprocity.thy\
+ NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy\
NumberTheory/ROOT.ML
@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
@@ -640,9 +641,9 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy \
- ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy \
- ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy \
- ex/Codegenerator.thy ex/Commutative_RingEx.thy \
+ ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/CodeCollections.thy \
+ ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy \
+ ex/Codegenerator.thy ex/Commutative_RingEx.thy \
ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy \
ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
@@ -652,10 +653,10 @@
ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
ex/Reflection.thy ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
ex/Records.thy ex/Reflected_Presburger.thy ex/Refute_Examples.thy \
- ex/SAT_Examples.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy ex/StringEx.thy \
+ ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \
ex/Sudoku.thy ex/Tarski.thy ex/document/root.bib ex/document/root.tex \
ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML ex/set.thy \
- ex/svc_funcs.ML ex/svc_test.ML ex/svc_test.thy
+ ex/svc_funcs.ML ex/svc_test.thy
@$(ISATOOL) usedir $(OUT)/HOL ex
@@ -755,7 +756,7 @@
$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML Nominal/Nominal.thy \
Nominal/nominal_atoms.ML Nominal/nominal_induct.ML \
- Nominal/nominal_package.ML Nominal/nominal_permeq.ML
+ Nominal/nominal_package.ML Nominal/nominal_permeq.ML Library/Infinite_Set.thy
@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal