changeset 39198 | f967a16dfcdd |
parent 38288 | 63425c4b5f57 |
child 39302 | d7728f65b353 |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 07 10:05:19 2010 +0200 @@ -110,7 +110,7 @@ "my_int_rel (x, y) (u, v) = (x + v = u + y)" quotient_type my_int = "nat \<times> nat" / my_int_rel -by (auto simp add: equivp_def expand_fun_eq) +by (auto simp add: equivp_def ext_iff) definition add_raw where "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"