1.1 --- a/src/HOL/IsaMakefile Wed Jul 20 10:11:08 2011 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed Jul 20 10:48:00 2011 +0200
1.3 @@ -444,25 +444,25 @@
1.4 Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
1.5 Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
1.6 Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
1.7 - Library/Code_Char_ord.thy Library/Code_Integer.thy Library/Code_Natural.thy \
1.8 - Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
1.9 - Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
1.10 - Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
1.11 - Library/Dlist_Cset.thy \
1.12 + Library/Code_Char_ord.thy Library/Code_Integer.thy \
1.13 + Library/Code_Natural.thy Library/Code_Prolog.thy \
1.14 + Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \
1.15 + Library/Continuity.thy Library/Convex.thy Library/Countable.thy \
1.16 + Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy \
1.17 Library/Efficient_Nat.thy Library/Eval_Witness.thy \
1.18 - Library/Executable_Set.thy Library/Extended_Reals.thy \
1.19 - Library/Float.thy Library/Formal_Power_Series.thy \
1.20 - Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Cset.thy \
1.21 - Library/FuncSet.thy Library/Function_Algebras.thy \
1.22 - Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
1.23 - Library/Indicator_Function.thy Library/Infinite_Set.thy \
1.24 - Library/Inner_Product.thy Library/Kleene_Algebra.thy \
1.25 - Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
1.26 - Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \
1.27 - Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
1.28 - Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
1.29 - Library/Multiset.thy Library/Nat_Bijection.thy \
1.30 - Library/Nat_Infinity.thy Library/Nested_Environment.thy \
1.31 + Library/Executable_Set.thy Library/Extended_Real.thy \
1.32 + Library/Extended_Nat.thy Library/Float.thy \
1.33 + Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
1.34 + Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \
1.35 + Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \
1.36 + Library/Glbs.thy Library/Indicator_Function.thy \
1.37 + Library/Infinite_Set.thy Library/Inner_Product.thy \
1.38 + Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \
1.39 + Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
1.40 + Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy \
1.41 + Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \
1.42 + Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \
1.43 + Library/Nat_Bijection.thy Library/Nested_Environment.thy \
1.44 Library/Numeral_Type.thy Library/OptionalSugar.thy \
1.45 Library/Order_Relation.thy Library/Permutation.thy \
1.46 Library/Permutations.thy Library/Poly_Deriv.thy \
1.47 @@ -481,7 +481,7 @@
1.48 Library/Sum_of_Squares/sos_wrapper.ML \
1.49 Library/Sum_of_Squares/sum_of_squares.ML \
1.50 Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
1.51 - Library/While_Combinator.thy Library/Zorn.thy \
1.52 + Library/While_Combinator.thy Library/Zorn.thy \
1.53 $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
1.54 Library/reflection.ML Library/reify_data.ML \
1.55 Library/document/root.bib Library/document/root.tex
1.56 @@ -1201,7 +1201,7 @@
1.57 Multivariate_Analysis/Topology_Euclidean_Space.thy \
1.58 Multivariate_Analysis/document/root.tex \
1.59 Multivariate_Analysis/normarith.ML Library/Glbs.thy \
1.60 - Library/Extended_Reals.thy Library/Indicator_Function.thy \
1.61 + Library/Extended_Real.thy Library/Indicator_Function.thy \
1.62 Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy \
1.63 Library/FrechetDeriv.thy Library/Product_Vector.thy \
1.64 Library/Product_plus.thy
1.65 @@ -1574,7 +1574,7 @@
1.66 HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
1.67
1.68 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
1.69 - Library/Nat_Infinity.thy \
1.70 + Library/Extended_Nat.thy \
1.71 HOLCF/Library/Defl_Bifinite.thy \
1.72 HOLCF/Library/Bool_Discrete.thy \
1.73 HOLCF/Library/Char_Discrete.thy \
1.74 @@ -1628,7 +1628,7 @@
1.75 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
1.76
1.77 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
1.78 - Library/Nat_Infinity.thy \
1.79 + Library/Extended_Nat.thy \
1.80 HOLCF/Library/Stream.thy \
1.81 HOLCF/FOCUS/Fstreams.thy \
1.82 HOLCF/FOCUS/Fstream.thy \