src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 29 10:33:14 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 29 10:33:15 2010 +0200
@@ -1511,6 +1511,13 @@
 
 thm test_uninterpreted_relation.equation
 
+text {* Trivial predicate *}
+
+inductive implies_itself :: "'a => bool"
+where
+  "implies_itself x ==> implies_itself x"
+
+code_pred implies_itself .
 
 
 end