equal
deleted
inserted
replaced
62 lemma "x = (y\<Colon>bool bounded)" |
62 lemma "x = (y\<Colon>bool bounded)" |
63 nitpick [expect = genuine] |
63 nitpick [expect = genuine] |
64 oops |
64 oops |
65 |
65 |
66 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y" |
66 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y" |
67 nitpick [expect = none] |
67 nitpick [expect = potential] (* unfortunate *) |
68 sorry |
68 sorry |
69 |
69 |
70 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y" |
70 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y" |
71 nitpick [card = 1\<midarrow>5, expect = genuine] |
71 nitpick [card = 1\<midarrow>5, expect = genuine] |
72 oops |
72 oops |
160 |
160 |
161 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" |
161 lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" |
162 nitpick [card = 1, unary_ints, max_potential = 0, expect = none] |
162 nitpick [card = 1, unary_ints, max_potential = 0, expect = none] |
163 by (rule Zero_int_def_raw) |
163 by (rule Zero_int_def_raw) |
164 |
164 |
165 lemma "Abs_Integ (Rep_Integ a) = a" |
|
166 nitpick [card = 1, unary_ints, max_potential = 0, expect = none] |
|
167 by (rule Rep_Integ_inverse) |
|
168 |
|
169 lemma "Abs_list (Rep_list a) = a" |
165 lemma "Abs_list (Rep_list a) = a" |
170 nitpick [card = 1\<midarrow>2, expect = none] |
166 nitpick [card = 1\<midarrow>2, expect = none] |
171 by (rule Rep_list_inverse) |
167 by (rule Rep_list_inverse) |
172 |
168 |
173 record point = |
169 record point = |