src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 56927 4044a7d1720f
parent 56679 5545bfdfefcc
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri May 09 08:13:36 2014 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri May 09 08:13:37 2014 +0200
     1.3 @@ -452,8 +452,8 @@
     1.4  values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
     1.5  values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
     1.6  
     1.7 -value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
     1.8 -value [code] "Predicate.the (slice ([]::int list))"
     1.9 +value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
    1.10 +value "Predicate.the (slice ([]::int list))"
    1.11  
    1.12  
    1.13  text {* tricky case with alternative rules *}
    1.14 @@ -830,7 +830,7 @@
    1.15  
    1.16  code_pred divmod_rel .
    1.17  thm divmod_rel.equation
    1.18 -value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
    1.19 +value "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
    1.20  
    1.21  subsection {* Transforming predicate logic into logic programs *}
    1.22