src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 39803 a8178a7b7b51
parent 39786 30c077288dfe
child 40100 98d74bbe8cd8
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 30 15:37:11 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 30 15:37:12 2010 +0200
     1.3 @@ -1538,5 +1538,11 @@
     1.4  
     1.5  code_pred implies_itself .
     1.6  
     1.7 +text {* Case expressions *}
     1.8 +
     1.9 +definition
    1.10 +  "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
    1.11 +
    1.12 +code_pred [inductify] map_pairs .
    1.13  
    1.14  end