--- a/src/HOL/IsaMakefile Wed Nov 08 22:24:54 2006 +0100
+++ b/src/HOL/IsaMakefile Wed Nov 08 23:11:13 2006 +0100
@@ -84,13 +84,13 @@
$(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML \
$(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
Tools/res_atpset.ML \
- Binomial.thy Code_Generator.thy Datatype.ML Datatype.thy \
+ Code_Generator.thy Datatype.ML Datatype.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 \
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/Presburger.thy Integ/cooper_dec.ML \
Integ/cooper_proof.ML Integ/reflected_presburger.ML \
Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML \
Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy \
@@ -182,7 +182,7 @@
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 \
- Library/Infinite_Set.thy
+ Library/Infinite_Set.thy Library/Parity.thy
@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
@@ -215,7 +215,8 @@
Library/Library/document/root.bib Library/While_Combinator.thy \
Library/Product_ord.thy Library/Char_ord.thy \
Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
- Library/Coinductive_List.thy Library/AssocList.thy
+ Library/Coinductive_List.thy Library/AssocList.thy \
+ Library/Parity.thy Library/GCD.thy Library/Binomial.thy
@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
@@ -656,7 +657,7 @@
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.thy
+ ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
@$(ISATOOL) usedir $(OUT)/HOL ex