changeset 39803 | a8178a7b7b51 |
parent 39786 | 30c077288dfe |
child 40100 | 98d74bbe8cd8 |
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 30 15:37:11 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 30 15:37:12 2010 +0200 @@ -1538,5 +1538,11 @@ code_pred implies_itself . +text {* Case expressions *} + +definition + "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)" + +code_pred [inductify] map_pairs . end