src/HOL/IsaMakefile
changeset 32733 71618deaf777
parent 32674 b629fbcc5313
child 32812 6a8663ff5e44
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 28 21:35:57 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 28 22:47:34 2009 +0200
     1.3 @@ -87,30 +87,31 @@
     1.4    $(SRC)/Provers/hypsubst.ML \
     1.5    $(SRC)/Provers/quantifier1.ML \
     1.6    $(SRC)/Provers/splitter.ML \
     1.7 -  $(SRC)/Tools/IsaPlanner/isand.ML \
     1.8 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
     1.9 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    1.10 -  $(SRC)/Tools/IsaPlanner/zipper.ML \
    1.11 -  $(SRC)/Tools/atomize_elim.ML \
    1.12 -  $(SRC)/Tools/auto_solve.ML \
    1.13    $(SRC)/Tools/Code/code_haskell.ML \
    1.14    $(SRC)/Tools/Code/code_ml.ML \
    1.15    $(SRC)/Tools/Code/code_preproc.ML \
    1.16    $(SRC)/Tools/Code/code_printer.ML \
    1.17    $(SRC)/Tools/Code/code_target.ML \
    1.18    $(SRC)/Tools/Code/code_thingol.ML \
    1.19 +  $(SRC)/Tools/Code_Generator.thy \
    1.20 +  $(SRC)/Tools/IsaPlanner/isand.ML \
    1.21 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
    1.22 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    1.23 +  $(SRC)/Tools/IsaPlanner/zipper.ML \
    1.24 +  $(SRC)/Tools/atomize_elim.ML \
    1.25 +  $(SRC)/Tools/auto_solve.ML \
    1.26    $(SRC)/Tools/coherent.ML \
    1.27 +  $(SRC)/Tools/cong_tac.ML \
    1.28    $(SRC)/Tools/eqsubst.ML \
    1.29    $(SRC)/Tools/induct.ML \
    1.30 +  $(SRC)/Tools/induct_tacs.ML \
    1.31    $(SRC)/Tools/intuitionistic.ML \
    1.32 -  $(SRC)/Tools/induct_tacs.ML \
    1.33 +  $(SRC)/Tools/more_conv.ML \
    1.34    $(SRC)/Tools/nbe.ML \
    1.35 +  $(SRC)/Tools/project_rule.ML \
    1.36    $(SRC)/Tools/quickcheck.ML \
    1.37 -  $(SRC)/Tools/project_rule.ML \
    1.38    $(SRC)/Tools/random_word.ML \
    1.39    $(SRC)/Tools/value.ML \
    1.40 -  $(SRC)/Tools/Code_Generator.thy \
    1.41 -  $(SRC)/Tools/more_conv.ML \
    1.42    HOL.thy \
    1.43    Tools/hologic.ML \
    1.44    Tools/recfun_codegen.ML \
    1.45 @@ -130,9 +131,9 @@
    1.46    Inductive.thy \
    1.47    Lattices.thy \
    1.48    Nat.thy \
    1.49 +  Option.thy \
    1.50    OrderedGroup.thy \
    1.51    Orderings.thy \
    1.52 -  Option.thy \
    1.53    Plain.thy \
    1.54    Power.thy \
    1.55    Predicate.thy \
    1.56 @@ -215,8 +216,8 @@
    1.57    Equiv_Relations.thy \
    1.58    Groebner_Basis.thy \
    1.59    Hilbert_Choice.thy \
    1.60 +  Int.thy \
    1.61    IntDiv.thy \
    1.62 -  Int.thy \
    1.63    List.thy \
    1.64    Main.thy \
    1.65    Map.thy \
    1.66 @@ -280,8 +281,8 @@
    1.67  
    1.68  $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
    1.69    Archimedean_Field.thy \
    1.70 +  Complex.thy \
    1.71    Complex_Main.thy \
    1.72 -  Complex.thy \
    1.73    Deriv.thy \
    1.74    Fact.thy \
    1.75    GCD.thy \
    1.76 @@ -294,18 +295,18 @@
    1.77    MacLaurin.thy \
    1.78    Nat_Transfer.thy \
    1.79    NthRoot.thy \
    1.80 +  PReal.thy \
    1.81 +  Parity.thy \
    1.82 +  RComplete.thy \
    1.83 +  Rational.thy \
    1.84 +  Real.thy \
    1.85 +  RealDef.thy \
    1.86 +  RealPow.thy \
    1.87 +  RealVector.thy \
    1.88    SEQ.thy \
    1.89    Series.thy \
    1.90    Taylor.thy \
    1.91    Transcendental.thy \
    1.92 -  Parity.thy \
    1.93 -  PReal.thy \
    1.94 -  Rational.thy \
    1.95 -  RComplete.thy \
    1.96 -  RealDef.thy \
    1.97 -  RealPow.thy \
    1.98 -  Real.thy \
    1.99 -  RealVector.thy \
   1.100    Tools/float_syntax.ML \
   1.101    Tools/transfer.ML \
   1.102    Tools/Qelim/ferrante_rackoff_data.ML \