equal
deleted
inserted
replaced
137 val real_numeral_ss = |
137 val real_numeral_ss = |
138 HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, |
138 HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, |
139 minus_numeral_one]; |
139 minus_numeral_one]; |
140 |
140 |
141 fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th); |
141 fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th); |
142 |
|
143 |
|
144 fun inst x t = read_instantiate_sg (sign_of RealBin.thy) [(x,t)]; |
|
145 |
142 |
146 |
143 |
147 (*Now insert some identities previously stated for 0r and 1r*) |
144 (*Now insert some identities previously stated for 0r and 1r*) |
148 |
145 |
149 (** RealDef & Real **) |
146 (** RealDef & Real **) |