Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adding values to show and ensure that values works with complex terms and restores numerals on natural numbers
authorbulwahn
Thu, 16 Sep 2010 13:49:12 +0200
changeset 39466 f3c5da707f30
parent 39465 fcff6903595f
child 39467 139c694299f6
adding values to show and ensure that values works with complex terms and restores numerals on natural numbers
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle