equal
deleted
inserted
replaced
42 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
42 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
43 lessD = lessD, (*Can't change lessD: the rats are dense!*) |
43 lessD = lessD, (*Can't change lessD: the rats are dense!*) |
44 neqE = neqE, |
44 neqE = neqE, |
45 simpset = simpset addsimps simps |
45 simpset = simpset addsimps simps |
46 addsimprocs simprocs}) #> |
46 addsimprocs simprocs}) #> |
47 arith_inj_const ("Nat.of_nat", HOLogic.natT --> ratT) #> |
47 arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #> |
48 arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT) |
48 arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT) |
49 |
49 |
50 end; |
50 end; |