1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Examples from the Nitpick Manual *}
     1.5  
     1.6  theory Manual_Nits
     1.7 -imports Main Coinductive_List RealDef
     1.8 +imports Main Coinductive_List Quotient_Product RealDef
     1.9  begin
    1.10  
    1.11  chapter {* 3. First Steps *}
    1.12 @@ -102,6 +102,21 @@
    1.13  nitpick [show_datatypes]
    1.14  oops
    1.15  
    1.16 +fun my_int_rel where
    1.17 +"my_int_rel (x, y) (u, v) = (x + v = u + y)"
    1.18 +
    1.19 +quotient_type my_int = "nat \<times> nat" / my_int_rel
    1.20 +by (auto simp add: equivp_def expand_fun_eq)
    1.21 +
    1.22 +definition add_raw where
    1.23 +"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
    1.24 +
    1.25 +quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
    1.26 +
    1.27 +lemma "add x y = add x x"
    1.28 +nitpick [show_datatypes]
    1.29 +oops
    1.30 +
    1.31  record point =
    1.32    Xcoord :: int
    1.33    Ycoord :: int