equal
deleted
inserted
replaced
34 mult_mono_thms = mult_mono_thms, |
34 mult_mono_thms = mult_mono_thms, |
35 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
35 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
36 lessD = lessD, (*Can't change lessD: the reals are dense!*) |
36 lessD = lessD, (*Can't change lessD: the reals are dense!*) |
37 neqE = neqE, |
37 neqE = neqE, |
38 simpset = simpset addsimps simps}) #> |
38 simpset = simpset addsimps simps}) #> |
39 arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #> |
39 arith_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #> |
40 arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT) |
40 arith_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT) |
41 |
41 |
42 end; |
42 end; |