src/HOL/IsaMakefile
changeset 43919 a7e4fb1a0502
parent 43834 6ce89c4ec141
child 43920 cedb5cb948fd
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 19 11:15:38 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 19 14:35:44 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/Extended_Nat.thy Library/Float.thy				\
    1.32 +  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    1.33 +  Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
    1.34 +  Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\
    1.35 +  Library/Glbs.thy Library/Indicator_Function.thy			\
    1.36 +  Library/Infinite_Set.thy Library/Inner_Product.thy			\
    1.37 +  Library/Kleene_Algebra.thy Library/LaTeXsugar.thy			\
    1.38 +  Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
    1.39 +  Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy	\
    1.40 +  Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy	\
    1.41 +  Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
    1.42 +  Library/Nat_Bijection.thy Library/Nested_Environment.thy		\
    1.43    Library/Numeral_Type.thy Library/OptionalSugar.thy			\
    1.44    Library/Order_Relation.thy Library/Permutation.thy			\
    1.45    Library/Permutations.thy Library/Poly_Deriv.thy			\
    1.46 @@ -481,7 +481,7 @@
    1.47    Library/Sum_of_Squares/sos_wrapper.ML					\
    1.48    Library/Sum_of_Squares/sum_of_squares.ML				\
    1.49    Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
    1.50 -  Library/While_Combinator.thy Library/Zorn.thy	\
    1.51 +  Library/While_Combinator.thy Library/Zorn.thy				\
    1.52    $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
    1.53    Library/reflection.ML Library/reify_data.ML				\
    1.54    Library/document/root.bib Library/document/root.tex
    1.55 @@ -1576,7 +1576,7 @@
    1.56  HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
    1.57  
    1.58  $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
    1.59 -  Library/Nat_Infinity.thy \
    1.60 +  Library/Extended_Nat.thy \
    1.61    HOLCF/Library/Defl_Bifinite.thy \
    1.62    HOLCF/Library/Bool_Discrete.thy \
    1.63    HOLCF/Library/Char_Discrete.thy \
    1.64 @@ -1630,7 +1630,7 @@
    1.65  HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
    1.66  
    1.67  $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
    1.68 -  Library/Nat_Infinity.thy \
    1.69 +  Library/Extended_Nat.thy \
    1.70    HOLCF/Library/Stream.thy \
    1.71    HOLCF/FOCUS/Fstreams.thy \
    1.72    HOLCF/FOCUS/Fstream.thy \