diff -r c7cbbb18eabe -r c7f5f0b7dc7f src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- 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