src/HOL/Real/real_arith.ML
changeset 10574 8f98f0301d67
parent 9436 62bb04ab4b01
child 10693 9e4a0e84d0d6
     1.1 --- a/src/HOL/Real/real_arith.ML	Fri Dec 01 19:44:48 2000 +0100
     1.2 +++ b/src/HOL/Real/real_arith.ML	Fri Dec 01 19:53:29 2000 +0100
     1.3 @@ -53,8 +53,9 @@
     1.4    "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
     1.5  
     1.6  val real_arith_setup =
     1.7 - [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
     1.8 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
     1.9     {add_mono_thms = add_mono_thms @ add_mono_thms_real,
    1.10 +    inj_thms = inj_thms, (*FIXME: add real*)
    1.11      lessD = lessD,  (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
    1.12      simpset = simpset addsimps simps@add_rules
    1.13                        addsimprocs simprocs