--- a/src/HOL/IsaMakefile Wed Aug 17 10:03:58 2011 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 17 13:14:20 2011 +0200
@@ -437,39 +437,35 @@
Library/Code_Char_ord.thy Library/Code_Integer.thy \
Library/Code_Natural.thy Library/Code_Prolog.thy \
Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \
- Library/Cset.thy Library/Cset_Monad.thy \
- Library/Continuity.thy Library/Convex.thy Library/Countable.thy \
- Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy \
- Library/Efficient_Nat.thy Library/Eval_Witness.thy \
- Library/Executable_Set.thy Library/Extended_Real.thy \
- Library/Extended_Nat.thy Library/Float.thy \
+ Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \
+ Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy \
+ Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy \
+ Library/Eval_Witness.thy Library/Executable_Set.thy \
+ Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \
- Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \
- Library/Glbs.thy Library/Indicator_Function.thy \
- Library/Infinite_Set.thy Library/Inner_Product.thy \
- Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \
- Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
- Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy \
- Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \
- Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \
- Library/Nat_Bijection.thy Library/Nested_Environment.thy \
- Library/Numeral_Type.thy Library/Old_Recdef.thy \
- Library/OptionalSugar.thy \
- Library/Order_Relation.thy Library/Permutation.thy \
- Library/Permutations.thy Library/Poly_Deriv.thy \
- Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \
- Library/Preorder.thy Library/Product_Vector.thy \
- Library/Product_ord.thy Library/Product_plus.thy \
- Library/Product_Lattice.thy \
- Library/Quickcheck_Types.thy \
- Library/Quotient_List.thy Library/Quotient_Option.thy \
- Library/Quotient_Product.thy Library/Quotient_Sum.thy \
- Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
- Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \
- Library/README.html \
- Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
- Library/Reflection.thy \
+ Library/Function_Algebras.thy \
+ Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
+ Library/Indicator_Function.thy Library/Infinite_Set.thy \
+ Library/Inner_Product.thy Library/Kleene_Algebra.thy \
+ Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
+ Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \
+ Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
+ Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
+ Library/Multiset.thy Library/Nat_Bijection.thy \
+ Library/Numeral_Type.thy Library/Old_Recdef.thy \
+ Library/OptionalSugar.thy Library/Order_Relation.thy \
+ Library/Permutation.thy Library/Permutations.thy \
+ Library/Poly_Deriv.thy Library/Polynomial.thy \
+ Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \
+ Library/Product_Vector.thy Library/Product_ord.thy \
+ Library/Product_plus.thy Library/Product_Lattice.thy \
+ Library/Quickcheck_Types.thy Library/Quotient_List.thy \
+ Library/Quotient_Option.thy Library/Quotient_Product.thy \
+ Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \
+ Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy \
+ Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy \
+ Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \
Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
@@ -830,9 +826,9 @@
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
-$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
- Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
- Unix/document/root.bib Unix/document/root.tex
+$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML \
+ Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib \
+ Unix/document/root.tex
@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix