src/HOL/IsaMakefile
changeset 32479 521cc9bf2958
parent 32402 5731300da417
child 32491 d5d8bea0cd94
child 32496 4ab00a2642c3
     1.1 --- a/src/HOL/IsaMakefile	Tue Sep 01 14:13:34 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -34,8 +34,8 @@
     1.4    HOL-Modelcheck \
     1.5    HOL-NanoJava \
     1.6    HOL-Nominal-Examples \
     1.7 -  HOL-NewNumberTheory \
     1.8 -  HOL-NumberTheory \
     1.9 +  HOL-Number_Theory \
    1.10 +  HOL-Old_Number_Theory \
    1.11    HOL-Prolog \
    1.12    HOL-SET-Protocol \
    1.13    HOL-SizeChange \
    1.14 @@ -282,11 +282,13 @@
    1.15    Complex.thy \
    1.16    Deriv.thy \
    1.17    Fact.thy \
    1.18 +  GCD.thy \
    1.19    Integration.thy \
    1.20    Lim.thy \
    1.21    Limits.thy \
    1.22    Ln.thy \
    1.23    Log.thy \
    1.24 +  Lubs.thy \
    1.25    MacLaurin.thy \
    1.26    NatTransfer.thy \
    1.27    NthRoot.thy \
    1.28 @@ -294,9 +296,7 @@
    1.29    Series.thy \
    1.30    Taylor.thy \
    1.31    Transcendental.thy \
    1.32 -  GCD.thy \
    1.33    Parity.thy \
    1.34 -  Lubs.thy \
    1.35    PReal.thy \
    1.36    Rational.thy \
    1.37    RComplete.thy \
    1.38 @@ -330,10 +330,10 @@
    1.39    Library/Finite_Cartesian_Product.thy Library/FrechetDeriv.thy		\
    1.40    Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
    1.41    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
    1.42 -  Library/Lattice_Syntax.thy Library/Legacy_GCD.thy			\
    1.43 +  Library/Lattice_Syntax.thy			\
    1.44    Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
    1.45    Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy	\
    1.46 -  Library/Permutation.thy Library/Primes.thy Library/Pocklington.thy	\
    1.47 +  Library/Permutation.thy	\
    1.48    Library/Quotient.thy Library/Quicksort.thy Library/Nat_Infinity.thy	\
    1.49    Library/Word.thy Library/README.html Library/Continuity.thy		\
    1.50    Library/Order_Relation.thy Library/Nested_Environment.thy		\
    1.51 @@ -487,38 +487,39 @@
    1.52  	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
    1.53  
    1.54  
    1.55 -## HOL-NewNumberTheory
    1.56 +## HOL-Number_Theory
    1.57  
    1.58 -HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
    1.59 +HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
    1.60  
    1.61 -$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
    1.62 +$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
    1.63    Library/Multiset.thy \
    1.64 -  NewNumberTheory/Binomial.thy \
    1.65 -  NewNumberTheory/Cong.thy \
    1.66 -  NewNumberTheory/Fib.thy \
    1.67 -  NewNumberTheory/MiscAlgebra.thy \
    1.68 -  NewNumberTheory/Residues.thy \
    1.69 -  NewNumberTheory/UniqueFactorization.thy  \
    1.70 -  NewNumberTheory/ROOT.ML
    1.71 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
    1.72 +  Number_Theory/Binomial.thy \
    1.73 +  Number_Theory/Cong.thy \
    1.74 +  Number_Theory/Fib.thy \
    1.75 +  Number_Theory/MiscAlgebra.thy \
    1.76 +  Number_Theory/Number_Theory.thy \
    1.77 +  Number_Theory/Residues.thy \
    1.78 +  Number_Theory/UniqueFactorization.thy  \
    1.79 +  Number_Theory/ROOT.ML
    1.80 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
    1.81  
    1.82  
    1.83 -## HOL-NumberTheory
    1.84 +## HOL-Old_Number_Theory
    1.85  
    1.86 -HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
    1.87 +HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
    1.88  
    1.89 -$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL Library/Permutation.thy		\
    1.90 -  Library/Primes.thy NumberTheory/Fib.thy				\
    1.91 -  NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy		\
    1.92 -  NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy			\
    1.93 -  NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy			\
    1.94 -  NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy		\
    1.95 -  NumberTheory/Finite2.thy NumberTheory/Int2.thy			\
    1.96 -  NumberTheory/EvenOdd.thy NumberTheory/Residues.thy			\
    1.97 -  NumberTheory/Euler.thy NumberTheory/Gauss.thy				\
    1.98 -  NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
    1.99 -  NumberTheory/ROOT.ML
   1.100 -	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NumberTheory
   1.101 +$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy		\
   1.102 +  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy				\
   1.103 +  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy		\
   1.104 +  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy			\
   1.105 +  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy			\
   1.106 +  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy		\
   1.107 +  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy			\
   1.108 +  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy			\
   1.109 +  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy				\
   1.110 +  Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
   1.111 +  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy Old_Number_Theory/ROOT.ML
   1.112 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
   1.113  
   1.114  
   1.115  ## HOL-Hoare
   1.116 @@ -573,7 +574,7 @@
   1.117    Library/FuncSet.thy \
   1.118    Library/Multiset.thy \
   1.119    Library/Permutation.thy \
   1.120 -  Library/Primes.thy \
   1.121 +  Number_Theory/Primes.thy \
   1.122    Algebra/AbelCoset.thy \
   1.123    Algebra/Bij.thy \
   1.124    Algebra/Congruence.thy \
   1.125 @@ -876,7 +877,7 @@
   1.126  HOL-ex: HOL $(LOG)/HOL-ex.gz
   1.127  
   1.128  $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy		\
   1.129 -  Library/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
   1.130 +  Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
   1.131    ex/Arith_Examples.thy				\
   1.132    ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
   1.133    ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\