changeset 38728 | 182b180e9804 |
parent 38727 | c7f5f0b7dc7f |
child 38731 | 2c8a595af43e |
--- 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