--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Mon Sep 26 10:30:37 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Mon Sep 26 10:57:20 2011 +0200
@@ -111,6 +111,19 @@
oops
*)
+subsection {* Simple examples with inductive predicates *}
+
+inductive even where
+ "even 0" |
+ "even n ==> even (Suc (Suc n))"
+
+code_pred even .
+
+lemma "even (n - 2) ==> even n"
+quickcheck[narrowing, expect = counterexample]
+oops
+
+
subsection {* AVL Trees *}
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat