equal
deleted
inserted
replaced
174 lemma "Abs_point_ext (Rep_point_ext a) = a" |
174 lemma "Abs_point_ext (Rep_point_ext a) = a" |
175 nitpick [expect = none] |
175 nitpick [expect = none] |
176 by (fact Rep_point_ext_inverse) |
176 by (fact Rep_point_ext_inverse) |
177 |
177 |
178 lemma "Fract a b = of_int a / of_int b" |
178 lemma "Fract a b = of_int a / of_int b" |
|
179 (* FIXME: broken by conversion of Rat.thy to lift_definition/transfer. |
179 nitpick [card = 1, expect = none] |
180 nitpick [card = 1, expect = none] |
|
181 *) |
180 by (rule Fract_of_int_quotient) |
182 by (rule Fract_of_int_quotient) |
181 |
183 |
182 lemma "Abs_Rat (Rep_Rat a) = a" |
184 lemma "Abs_rat (Rep_rat a) = a" |
183 nitpick [card = 1, expect = none] |
185 nitpick [card = 1, expect = none] |
184 by (rule Rep_Rat_inverse) |
186 by (rule Rep_rat_inverse) |
185 |
187 |
186 end |
188 end |