--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 22 14:36:10 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Feb 22 19:31:00 2010 +0100
@@ -8,7 +8,7 @@
header {* Examples from the Nitpick Manual *}
theory Manual_Nits
-imports Main Coinductive_List RealDef
+imports Main Coinductive_List Quotient_Product RealDef
begin
chapter {* 3. First Steps *}
@@ -102,6 +102,21 @@
nitpick [show_datatypes]
oops
+fun my_int_rel where
+"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)
+
+definition add_raw where
+"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
+
+quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
+
+lemma "add x y = add x x"
+nitpick [show_datatypes]
+oops
+
record point =
Xcoord :: int
Ycoord :: int