1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 29 10:33:15 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,25 @@
     1.4  
     1.5  thm test_uninterpreted_relation.equation
     1.6  
     1.7 +inductive list_ex'
     1.8 +where
     1.9 +  "P x ==> list_ex' P (x#xs)"
    1.10 +| "list_ex' P xs ==> list_ex' P (x#xs)"
    1.11 +
    1.12 +code_pred list_ex' .
    1.13 +
    1.14 +inductive test_uninterpreted_relation2 :: "('a => bool) => 'a list => bool"
    1.15 +where
    1.16 +  "list_ex r xs ==> test_uninterpreted_relation2 r xs"
    1.17 +| "list_ex' r xs ==> test_uninterpreted_relation2 r xs"
    1.18 +
    1.19 +text {* Proof procedure cannot handle this situation yet. *}
    1.20 +
    1.21 +code_pred (modes: i => i => bool) [skip_proof] test_uninterpreted_relation2 .
    1.22 +
    1.23 +thm test_uninterpreted_relation2.equation
    1.24 +
    1.25 +
    1.26  text {* Trivial predicate *}
    1.27  
    1.28  inductive implies_itself :: "'a => bool"