# HG changeset patch
# User bulwahn
# Date 1285749195 -7200
# Node ID cfd06840f477a6ae605ba009c9cd75434b22bd4e
# Parent  a8c52b982ff20e026c8e42d5c35e5d4926611a94
added a test case to Predicate_Compile_Tests

diff -r a8c52b982ff2 -r cfd06840f477 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