moved Infinite_Set.thy to Library;
removed obsolete ex/StringEx.thy;
renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;

--- 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