src/HOL/IsaMakefile
changeset 31100 6a2e67fe4488
parent 31068 f591144b0f17
child 31117 527ba4a37843
child 31125 80218ee73167
     1.1 --- a/src/HOL/IsaMakefile	Mon May 11 11:53:21 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon May 11 15:18:32 2009 +0200
     1.3 @@ -295,8 +295,6 @@
     1.4    Real.thy \
     1.5    RealVector.thy \
     1.6    Tools/float_syntax.ML \
     1.7 -  Tools/rat_arith.ML \
     1.8 -  Tools/real_arith.ML \
     1.9    Tools/Qelim/ferrante_rackoff_data.ML \
    1.10    Tools/Qelim/ferrante_rackoff.ML \
    1.11    Tools/Qelim/langford_data.ML \
    1.12 @@ -1051,7 +1049,6 @@
    1.13    NSA/HyperDef.thy \
    1.14    NSA/HyperNat.thy \
    1.15    NSA/Hyperreal.thy \
    1.16 -  NSA/hypreal_arith.ML \
    1.17    NSA/Filter.thy \
    1.18    NSA/NatStar.thy \
    1.19    NSA/NSA.thy \