| changeset 39466 | f3c5da707f30 |
| parent 39463 | 7ce0ed8dc4d6 |
| child 39800 | 17e29ddd538e |
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 16 13:49:11 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 16 13:49:12 2010 +0200 @@ -19,6 +19,8 @@ values "{(x, y, z). append x y z}" +values 4 "{(z, x, y). append x y ((1::nat) # (2 # (3 # z)))}" + values 3 "{(x, y, z). append x y z}" setup {* Code_Prolog.map_code_options (K