src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 56679 5545bfdfefcc
parent 55932 68c5104d2204
child 56927 4044a7d1720f
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 24 00:08:48 2014 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 24 00:23:38 2014 +0200
     1.3 @@ -1077,12 +1077,12 @@
     1.4  *)
     1.5  subsection {* Inverting list functions *}
     1.6  
     1.7 -code_pred [inductify, skip_proof] size_list .
     1.8 -code_pred [new_random_dseq inductify] size_list .
     1.9 -thm size_listP.equation
    1.10 -thm size_listP.new_random_dseq_equation
    1.11 +code_pred [inductify, skip_proof] size_list' .
    1.12 +code_pred [new_random_dseq inductify] size_list' .
    1.13 +thm size_list'P.equation
    1.14 +thm size_list'P.new_random_dseq_equation
    1.15  
    1.16 -values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
    1.17 +values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}"
    1.18  
    1.19  code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
    1.20  thm concatP.equation