diff -r 7186d338f2e1 -r 2a35950ec495 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 23 14:50:14 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 23 14:50:14 2010 +0200
@@ -36,6 +36,21 @@
 quickcheck[generator=predicate_compile_wo_ff]
 oops
 
+section {* Equivalences *}
+
+inductive is_ten :: "nat => bool"
+where
+  "is_ten 10"
+
+inductive is_eleven :: "nat => bool"
+where
+  "is_eleven 11"
+
+lemma
+  "is_ten x = is_eleven x"
+quickcheck[generator = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
+oops
+
 section {* Context Free Grammar *}
 
 datatype alphabet = a | b