--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 20:04:49 2010 +0800
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 16:59:46 2010 +0200
@@ -173,4 +173,18 @@
values "{e. log10 e}"
values "{e. times10 e}"
+section {* Example negation *}
+
+datatype abc = A | B | C
+
+inductive notB :: "abc => bool"
+where
+ "y \<noteq> B \<Longrightarrow> notB y"
+
+code_pred notB .
+
+ML {* Code_Prolog.options := {ensure_groundness = true} *}
+
+values 2 "{y. notB y}"
+
end