| changeset 38075 | 3d5e2b7d1374 |
| parent 38074 | 31174744b9a2 |
| child 38080 | 8c20eb9a388d |
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Jul 29 17:27:54 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Jul 29 17:27:55 2010 +0200 @@ -20,4 +20,6 @@ Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"] *} +values "{(x, y, z). append x y z}" + end