Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added a test case to Predicate_Compile_Tests
authorbulwahn
Wed, 29 Sep 2010 10:33:15 +0200
changeset 39784 cfd06840f477
parent 39783 a8c52b982ff2
child 39785 05c4e9ecf5f6
added a test case to Predicate_Compile_Tests
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle