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.
confine term setup to Eval serialiser
authorhaftmann
Wed, 06 May 2009 16:01:05 +0200
changeset 31046 c1969f609bf7
parent 31045 f0c7607bb295
child 31047 c13b0406c039
confine term setup to Eval serialiser
src/HOL/Library/Code_Char.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Code_Char.thy	Wed May 06 16:01:05 2009 +0200
+++ b/src/HOL/Library/Code_Char.thy	Wed May 06 16:01:05 2009 +0200
@@ -33,6 +33,6 @@
   (Haskell infixl 4 "==")
 
 code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
-  (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
+  (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
 
 end
isabelle