src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy

--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:46 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Wed Aug 25 16:59:48 2010 +0200
@@ -187,4 +187,12 @@
 
 values 2 "{y. notB y}"
 
+inductive notAB :: "abc * abc \<Rightarrow> bool"
+where
+  "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
+
+code_pred notAB .
+
+values 5 "{y. notAB y}"
+
 end