src/HOL/IsaMakefile
changeset 28952 15a4b2cf8c34
parent 28905 c999579a5166
child 29026 5fbaa05f637f
     1.1 --- a/src/HOL/IsaMakefile	Wed Dec 03 09:53:58 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -99,6 +99,7 @@
     1.4    SAT.thy \
     1.5    Set.thy \
     1.6    Sum_Type.thy \
     1.7 +  Tools/arith_data.ML \
     1.8    Tools/cnf_funcs.ML \
     1.9    Tools/datatype_abs_proofs.ML \
    1.10    Tools/datatype_aux.ML \
    1.11 @@ -124,6 +125,7 @@
    1.12    Tools/function_package/pattern_split.ML \
    1.13    Tools/function_package/size.ML \
    1.14    Tools/function_package/sum_tree.ML \
    1.15 +  Tools/hologic.ML \
    1.16    Tools/inductive_codegen.ML \
    1.17    Tools/inductive_package.ML \
    1.18    Tools/inductive_realizer.ML \
    1.19 @@ -139,6 +141,7 @@
    1.20    Tools/rewrite_hol_proof.ML \
    1.21    Tools/sat_funcs.ML \
    1.22    Tools/sat_solver.ML \
    1.23 +  Tools/simpdata.ML \
    1.24    Tools/split_rule.ML \
    1.25    Tools/typecopy_package.ML \
    1.26    Tools/typedef_codegen.ML \
    1.27 @@ -146,9 +149,6 @@
    1.28    Transitive_Closure.thy \
    1.29    Typedef.thy \
    1.30    Wellfounded.thy \
    1.31 -  arith_data.ML \
    1.32 -  hologic.ML \
    1.33 -  simpdata.ML \
    1.34    $(SRC)/Provers/Arith/abel_cancel.ML \
    1.35    $(SRC)/Provers/Arith/cancel_div_mod.ML \
    1.36    $(SRC)/Provers/Arith/cancel_sums.ML \
    1.37 @@ -170,6 +170,7 @@
    1.38    $(SRC)/Tools/IsaPlanner/zipper.ML \
    1.39    $(SRC)/Tools/atomize_elim.ML \
    1.40    $(SRC)/Tools/code/code_funcgr.ML \
    1.41 +  $(SRC)/Tools/code/code_funcgr.ML \
    1.42    $(SRC)/Tools/code/code_name.ML \
    1.43    $(SRC)/Tools/code/code_printer.ML \
    1.44    $(SRC)/Tools/code/code_target.ML \
    1.45 @@ -189,20 +190,18 @@
    1.46    Arith_Tools.thy \
    1.47    ATP_Linkup.thy \
    1.48    Code_Eval.thy \
    1.49 +  Code_Message.thy \
    1.50    Equiv_Relations.thy \
    1.51    Groebner_Basis.thy \
    1.52    Hilbert_Choice.thy \
    1.53 -  int_arith1.ML \
    1.54    IntDiv.thy \
    1.55 -  int_factor_simprocs.ML \
    1.56    Int.thy \
    1.57 -  Library/RType.thy \
    1.58 +  Typerep.thy \
    1.59    List.thy \
    1.60    Main.thy \
    1.61    Map.thy \
    1.62    NatBin.thy \
    1.63    Nat_Int_Bij.thy \
    1.64 -  nat_simprocs.ML \
    1.65    Presburger.thy \
    1.66    Recdef.thy \
    1.67    Relation_Power.thy \
    1.68 @@ -213,6 +212,9 @@
    1.69    $(SRC)/Provers/Arith/combine_numerals.ML \
    1.70    $(SRC)/Provers/Arith/extract_common_term.ML \
    1.71    $(SRC)/Tools/Metis/metis.ML \
    1.72 +  Tools/int_arith.ML \
    1.73 +  Tools/int_factor_simprocs.ML \
    1.74 +  Tools/nat_simprocs.ML \
    1.75    Tools/Groebner_Basis/groebner.ML \
    1.76    Tools/Groebner_Basis/misc.ML \
    1.77    Tools/Groebner_Basis/normalizer_data.ML \
    1.78 @@ -251,38 +253,39 @@
    1.79  	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    1.80  
    1.81  $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
    1.82 -  Complex/Complex_Main.thy \
    1.83 -  Complex/Complex.thy \
    1.84 +  Complex_Main.thy \
    1.85 +  Complex.thy \
    1.86    Complex/Fundamental_Theorem_Algebra.thy \
    1.87 -  Hyperreal/Deriv.thy \
    1.88 -  Hyperreal/Fact.thy \
    1.89 -  Hyperreal/Integration.thy \
    1.90 -  Hyperreal/Lim.thy \
    1.91 -  Hyperreal/Ln.thy \
    1.92 -  Hyperreal/Log.thy \
    1.93 -  Hyperreal/MacLaurin.thy \
    1.94 -  Hyperreal/NthRoot.thy \
    1.95 +  Deriv.thy \
    1.96 +  Fact.thy \
    1.97 +  FrechetDeriv.thy \
    1.98 +  Integration.thy \
    1.99 +  Lim.thy \
   1.100 +  Ln.thy \
   1.101 +  Log.thy \
   1.102 +  MacLaurin.thy \
   1.103 +  NthRoot.thy \
   1.104    Hyperreal/SEQ.thy \
   1.105 -  Hyperreal/Series.thy \
   1.106 -  Hyperreal/Taylor.thy \
   1.107 -  Hyperreal/Transcendental.thy \
   1.108 +  Series.thy \
   1.109 +  Taylor.thy \
   1.110 +  Transcendental.thy \
   1.111    Library/Dense_Linear_Order.thy \
   1.112 -  Library/GCD.thy \
   1.113 -  Library/Order_Relation.thy \
   1.114 -  Library/Parity.thy \
   1.115 -  Library/Univ_Poly.thy \
   1.116 -  Real/ContNotDenum.thy \
   1.117 -  Real/float_syntax.ML \
   1.118 -  Real/Lubs.thy \
   1.119 -  Real/PReal.thy \
   1.120 -  Real/rat_arith.ML \
   1.121 -  Real/Rational.thy \
   1.122 -  Real/RComplete.thy \
   1.123 -  Real/real_arith.ML \
   1.124 -  Real/RealDef.thy \
   1.125 -  Real/RealPow.thy \
   1.126 -  Real/Real.thy \
   1.127 +  GCD.thy \
   1.128 +  Order_Relation.thy \
   1.129 +  Parity.thy \
   1.130 +  Univ_Poly.thy \
   1.131 +  ContNotDenum.thy \
   1.132 +  Lubs.thy \
   1.133 +  PReal.thy \
   1.134 +  Rational.thy \
   1.135 +  RComplete.thy \
   1.136 +  RealDef.thy \
   1.137 +  RealPow.thy \
   1.138 +  Real.thy \
   1.139    Real/RealVector.thy \
   1.140 +  Tools/float_syntax.ML \
   1.141 +  Tools/rat_arith.ML \
   1.142 +  Tools/real_arith.ML \
   1.143    Tools/Qelim/ferrante_rackoff_data.ML \
   1.144    Tools/Qelim/ferrante_rackoff.ML \
   1.145    Tools/Qelim/langford_data.ML \
   1.146 @@ -315,13 +318,12 @@
   1.147    Library/Binomial.thy Library/Eval_Witness.thy	\
   1.148    Library/Code_Index.thy Library/Code_Char.thy				\
   1.149    Library/Code_Char_chr.thy Library/Code_Integer.thy			\
   1.150 -  Library/Code_Message.thy			\
   1.151    Library/Numeral_Type.thy			\
   1.152 -  Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy	\
   1.153 +  Library/Boolean_Algebra.thy Library/Countable.thy	\
   1.154    Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy		\
   1.155    Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
   1.156    Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
   1.157 -  Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
   1.158 +  Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML
   1.159  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
   1.160  
   1.161  
   1.162 @@ -793,11 +795,12 @@
   1.163    ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
   1.164    ex/svc_funcs.ML ex/svc_test.thy	\
   1.165    ex/ImperativeQuicksort.thy	\
   1.166 -  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy			\
   1.167 -  Complex/ex/Sqrt.thy							\
   1.168 -  Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
   1.169 -  Complex/ex/ReflectedFerrack.thy					\
   1.170 -  Complex/ex/linrtac.ML
   1.171 +  ex/BigO_Complex.thy			\
   1.172 +  ex/Arithmetic_Series_Complex.thy ex/HarmonicSeries.thy	\
   1.173 +  ex/Sqrt.thy							\
   1.174 +  ex/Sqrt_Script.thy ex/MIR.thy ex/mirtac.ML	\
   1.175 +  ex/ReflectedFerrack.thy					\
   1.176 +  ex/linrtac.ML
   1.177  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
   1.178  
   1.179  
   1.180 @@ -942,7 +945,7 @@
   1.181  HOL-Word: HOL $(OUT)/HOL-Word
   1.182  
   1.183  $(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Infinite_Set.thy	\
   1.184 -  Library/Parity.thy Library/Boolean_Algebra.thy			\
   1.185 +  Library/Boolean_Algebra.thy			\
   1.186    Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy		\
   1.187    Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy		\
   1.188    Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy	\