src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 39784 cfd06840f477
parent 39765 19cb8d558166
child 39786 30c077288dfe
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 29 10:33:14 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 29 10:33:15 2010 +0200
     1.3 @@ -1511,6 +1511,13 @@
     1.4  
     1.5  thm test_uninterpreted_relation.equation
     1.6  
     1.7 +text {* Trivial predicate *}
     1.8 +
     1.9 +inductive implies_itself :: "'a => bool"
    1.10 +where
    1.11 +  "implies_itself x ==> implies_itself x"
    1.12 +
    1.13 +code_pred implies_itself .
    1.14  
    1.15  
    1.16  end