1.1 --- a/src/HOL/IsaMakefile Wed Aug 05 17:10:10 2009 +0200
1.2 +++ b/src/HOL/IsaMakefile Thu Aug 06 19:51:59 2009 +0200
1.3 @@ -316,49 +316,45 @@
1.4
1.5 HOL-Library: HOL $(LOG)/HOL-Library.gz
1.6
1.7 -
1.8 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy \
1.9 - Library/Abstract_Rat.thy \
1.10 - Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \
1.11 - Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML \
1.12 - Library/Fset.thy Library/Convex_Euclidean_Space.thy \
1.13 - Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
1.14 - Library/Executable_Set.thy Library/Infinite_Set.thy \
1.15 - Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
1.16 - Library/Bit.thy Library/Topology_Euclidean_Space.thy \
1.17 - Library/Finite_Cartesian_Product.thy \
1.18 - Library/FrechetDeriv.thy Library/Fraction_Field.thy\
1.19 - Library/Fundamental_Theorem_Algebra.thy \
1.20 - Library/Inner_Product.thy Library/Kleene_Algebra.thy Library/Lattice_Syntax.thy \
1.21 - Library/Legacy_GCD.thy \
1.22 - Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy Library/State_Monad.thy \
1.23 - Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy \
1.24 - Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \
1.25 - Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \
1.26 - Library/README.html Library/Continuity.thy Library/Order_Relation.thy \
1.27 - Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \
1.28 - Library/Library/ROOT.ML Library/Library/document/root.tex \
1.29 - Library/Library/document/root.bib Library/While_Combinator.thy \
1.30 - Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
1.31 - Library/Option_ord.thy Library/Sublist_Order.thy \
1.32 - Library/List_lexord.thy Library/Commutative_Ring.thy \
1.33 - Library/comm_ring.ML Library/Coinductive_List.thy \
1.34 - Library/AssocList.thy Library/Formal_Power_Series.thy \
1.35 - Library/Binomial.thy Library/Eval_Witness.thy \
1.36 - Library/Code_Char.thy \
1.37 + Library/Abstract_Rat.thy Library/BigO.thy Library/ContNotDenum.thy \
1.38 + Library/Efficient_Nat.thy Library/Euclidean_Space.thy \
1.39 + Library/Sum_Of_Squares.thy Library/Sum_Of_Squares/sos_wrapper.ML \
1.40 + Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \
1.41 + Library/Convex_Euclidean_Space.thy Library/Glbs.thy \
1.42 + Library/normarith.ML Library/Executable_Set.thy \
1.43 + Library/Infinite_Set.thy Library/FuncSet.thy \
1.44 + Library/Permutations.thy Library/Determinants.thy Library/Bit.thy \
1.45 + Library/Topology_Euclidean_Space.thy \
1.46 + Library/Finite_Cartesian_Product.thy Library/FrechetDeriv.thy \
1.47 + Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \
1.48 + Library/Inner_Product.thy Library/Kleene_Algebra.thy \
1.49 + Library/Lattice_Syntax.thy Library/Legacy_GCD.thy \
1.50 + Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
1.51 + Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy \
1.52 + Library/Permutation.thy Library/Primes.thy Library/Pocklington.thy \
1.53 + Library/Quotient.thy Library/Quicksort.thy Library/Nat_Infinity.thy \
1.54 + Library/Word.thy Library/README.html Library/Continuity.thy \
1.55 + Library/Order_Relation.thy Library/Nested_Environment.thy \
1.56 + Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
1.57 + Library/Library/document/root.tex Library/Library/document/root.bib \
1.58 + Library/While_Combinator.thy Library/Product_ord.thy \
1.59 + Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy \
1.60 + Library/Sublist_Order.thy Library/List_lexord.thy \
1.61 + Library/Commutative_Ring.thy Library/comm_ring.ML \
1.62 + Library/Coinductive_List.thy Library/AssocList.thy \
1.63 + Library/Formal_Power_Series.thy Library/Binomial.thy \
1.64 + Library/Eval_Witness.thy Library/Code_Char.thy \
1.65 Library/Code_Char_chr.thy Library/Code_Integer.thy \
1.66 Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy \
1.67 Library/Boolean_Algebra.thy Library/Countable.thy \
1.68 Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy \
1.69 - Library/Poly_Deriv.thy \
1.70 - Library/Polynomial.thy \
1.71 - Library/Preorder.thy \
1.72 - Library/Product_plus.thy \
1.73 - Library/Product_Vector.thy \
1.74 - Library/Tree.thy \
1.75 - Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
1.76 - Library/reify_data.ML Library/reflection.ML \
1.77 - Library/LaTeXsugar.thy Library/OptionalSugar.thy
1.78 + Library/Poly_Deriv.thy Library/Polynomial.thy Library/Preorder.thy \
1.79 + Library/Product_plus.thy Library/Product_Vector.thy Library/Tree.thy \
1.80 + Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML \
1.81 + $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
1.82 + Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
1.83 + Library/OptionalSugar.thy
1.84 @cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
1.85
1.86