--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sun Apr 14 21:54:45 2013 +1000
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Mon Apr 15 10:41:03 2013 +0200
@@ -183,4 +183,14 @@
nitpick [card = 1, expect = none]
by (rule Rep_rat_inverse)
+typedef check = "{x\<Colon>nat. x < 2}" by (rule exI[of _ 0], auto)
+
+lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 2"
+nitpick [card = 1\<emdash>3, expect = none]
+using Rep_check[of "Abs_check n"] by auto
+
+lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 1"
+nitpick [card = 1\<emdash>3, expect = genuine]
+oops
+
end