src/HOL/Real/real_arith.ML
changeset 18708 4b3dadb4fe33
parent 17876 b9c92f384109
child 20254 58b71535ed00
     1.1 --- a/src/HOL/Real/real_arith.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Real/real_arith.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -118,16 +118,16 @@
     1.4    Fast_Arith.lin_arith_prover;
     1.5  
     1.6  val real_arith_setup =
     1.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.8 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.9     {add_mono_thms = add_mono_thms,
    1.10      mult_mono_thms = mult_mono_thms,
    1.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    1.12      lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
    1.13      neqE = neqE,
    1.14 -    simpset = simpset addsimps simps}),
    1.15 -  arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
    1.16 -  arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
    1.17 -  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)];
    1.18 +    simpset = simpset addsimps simps}) #>
    1.19 +  arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
    1.20 +  arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT) #>
    1.21 +  (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy));
    1.22  
    1.23  (* some thms for injection nat => real:
    1.24  real_of_nat_zero