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.
Repaired term_of_char.
authorberghofe
Thu, 02 Aug 2007 17:31:10 +0200
changeset 24130 5ab8044b6d46
parent 24129 591394d9ee66
child 24131 1099f6c73649
Repaired term_of_char.
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Thu Aug 02 17:29:40 2007 +0200
+++ b/src/HOL/List.thy	Thu Aug 02 17:31:10 2007 +0200
@@ -2790,7 +2790,7 @@
 *}
   "char" ("string")
 attach (term_of) {*
-val term_of_char = HOLogic.mk_char;
+val term_of_char = HOLogic.mk_char o ord;
 *}
 attach (test) {*
 fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
isabelle