--- a/src/HOL/Library/Code_Char.thy Tue Sep 16 09:21:22 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy Tue Sep 16 09:21:24 2008 +0200
@@ -6,19 +6,11 @@
header {* Code generation of pretty characters (and strings) *}
theory Code_Char
-imports Plain "~~/src/HOL/List"
+imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
begin
declare char.recs [code func del] char.cases [code func del]
-lemma [code func]:
- "size (c\<Colon>char) = 0"
- by (cases c) simp
-
-lemma [code func]:
- "char_size (c\<Colon>char) = 0"
- by (cases c) simp
-
code_type char
(SML "char")
(OCaml "char")
@@ -43,4 +35,10 @@
(OCaml "!((_ : char) = _)")
(Haskell infixl 4 "==")
+lemma [code func, code func del]:
+ "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
+
+code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
+ (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
+
end