equal
deleted
inserted
replaced
143 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)" |
143 lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)" |
144 nitpick [show_datatypes, expect = genuine] |
144 nitpick [show_datatypes, expect = genuine] |
145 oops |
145 oops |
146 |
146 |
147 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2" |
147 lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2" |
148 (* FIXME: broken by conversion of RealDef.thy to lift_definition/transfer. |
|
149 nitpick [show_datatypes, expect = genuine] |
148 nitpick [show_datatypes, expect = genuine] |
150 *) |
|
151 oops |
149 oops |
152 |
150 |
153 subsection {* 2.8. Inductive and Coinductive Predicates *} |
151 subsection {* 2.8. Inductive and Coinductive Predicates *} |
154 |
152 |
155 inductive even where |
153 inductive even where |