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.
fixed term_of_list;
authorwenzelm
Sun, 10 Dec 2006 20:09:08 +0100
changeset 21760 78248dda3a90
parent 21759 f4b20360751f
child 21761 d4fd9bb0ccd6
fixed term_of_list;
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Sun Dec 10 19:37:30 2006 +0100
+++ b/src/HOL/List.thy	Sun Dec 10 20:09:08 2006 +0100
@@ -2526,7 +2526,7 @@
 types_code
   "list" ("_ list")
 attach (term_of) {*
-val term_of_list = HOLogic.mk_list;
+fun term_of_list f T = HOLogic.mk_list T o map f;
 *}
 attach (test) {*
 fun gen_list' aG i j = frequency
isabelle