changeset 61076 | bdc1e2f0a86a |
parent 60500 | 903bb1495239 |
child 61585 | a9599d3d7610 |
--- a/src/HOL/Library/Code_Char.thy Tue Sep 01 17:25:36 2015 +0200 +++ b/src/HOL/Library/Code_Char.thy Tue Sep 01 22:32:58 2015 +0200 @@ -28,7 +28,7 @@ and (OCaml) "!((_ : char) = _)" and (Haskell) infix 4 "==" and (Scala) infixl 5 "==" -| constant "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" \<rightharpoonup> +| constant "Code_Evaluation.term_of :: char \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))" code_reserved SML