adjusted
authorhaftmann
Thu May 20 16:35:53 2010 +0200 (2010-05-20)
changeset 3702187c696bfe839
parent 37020 6c699a8e6927
child 37022 f9681d9d1d56
adjusted
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Thu May 20 16:35:52 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu May 20 16:35:53 2010 +0200
     1.3 @@ -401,16 +401,16 @@
     1.4    Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy			\
     1.5    Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML		\
     1.6    Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy		\
     1.7 -  Library/Glbs.thy Library/Executable_Set.thy	\
     1.8 +  Library/Glbs.thy Library/Executable_Set.thy				\
     1.9    Library/Infinite_Set.thy Library/FuncSet.thy				\
    1.10    Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy	\
    1.11    Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
    1.12    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
    1.13    Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
    1.14    Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
    1.15 -  Library/State_Monad.thy Library/Multiset.thy Library/Permutation.thy	\
    1.16 +  Library/More_List.thy Library/Multiset.thy Library/Permutation.thy	\
    1.17    Library/Quotient_Type.thy Library/Quicksort.thy			\
    1.18 -  Library/Nat_Infinity.thy Library/README.html				\
    1.19 +  Library/Nat_Infinity.thy Library/README.html	Library/State_Monad.thy	\
    1.20    Library/Continuity.thy Library/Order_Relation.thy			\
    1.21    Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy	\
    1.22    Library/Library/ROOT.ML Library/Library/document/root.tex		\
    1.23 @@ -433,7 +433,7 @@
    1.24    Library/Nat_Bijection.thy $(SRC)/Tools/float.ML			\
    1.25    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
    1.26    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
    1.27 -  Library/OptionalSugar.thy Library/Convex.thy                          \
    1.28 +  Library/OptionalSugar.thy Library/Convex.thy				\
    1.29    Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
    1.30  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.31  
    1.32 @@ -586,17 +586,18 @@
    1.33  
    1.34  HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
    1.35  
    1.36 -$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy		\
    1.37 -  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy				\
    1.38 -  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy		\
    1.39 -  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy			\
    1.40 -  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy			\
    1.41 -  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy		\
    1.42 -  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy			\
    1.43 -  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy			\
    1.44 -  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy				\
    1.45 +$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy	\
    1.46 +  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy		\
    1.47 +  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
    1.48 +  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy	\
    1.49 +  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy		\
    1.50 +  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy	\
    1.51 +  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy		\
    1.52 +  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy		\
    1.53 +  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy		\
    1.54    Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
    1.55 -  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy Old_Number_Theory/ROOT.ML
    1.56 +  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy	\
    1.57 +  Old_Number_Theory/ROOT.ML
    1.58  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
    1.59  
    1.60  
    1.61 @@ -711,9 +712,9 @@
    1.62  HOL-Auth: HOL $(LOG)/HOL-Auth.gz
    1.63  
    1.64  $(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
    1.65 -  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy		\
    1.66 -  Auth/Guard/Auth_Guard_Shared.thy		\
    1.67 -  Auth/Guard/Auth_Guard_Public.thy		\
    1.68 +  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy	\
    1.69 +  Auth/Guard/Auth_Guard_Shared.thy					\
    1.70 +  Auth/Guard/Auth_Guard_Public.thy					\
    1.71    Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy		\
    1.72    Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
    1.73    Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\