src/HOL/Library/Code_Char.thy
changeset 28228 7ebe8dc06cbb
parent 28090 29af3c712d2b
child 28244 f433e544a855
     1.1 --- a/src/HOL/Library/Code_Char.thy	Tue Sep 16 09:21:22 2008 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Sep 16 09:21:24 2008 +0200
     1.3 @@ -6,19 +6,11 @@
     1.4  header {* Code generation of pretty characters (and strings) *}
     1.5  
     1.6  theory Code_Char
     1.7 -imports Plain "~~/src/HOL/List"
     1.8 +imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
     1.9  begin
    1.10  
    1.11  declare char.recs [code func del] char.cases [code func del]
    1.12  
    1.13 -lemma [code func]:
    1.14 -  "size (c\<Colon>char) = 0"
    1.15 -  by (cases c) simp
    1.16 -
    1.17 -lemma [code func]:
    1.18 -  "char_size (c\<Colon>char) = 0"
    1.19 -  by (cases c) simp
    1.20 -
    1.21  code_type char
    1.22    (SML "char")
    1.23    (OCaml "char")
    1.24 @@ -43,4 +35,10 @@
    1.25    (OCaml "!((_ : char) = _)")
    1.26    (Haskell infixl 4 "==")
    1.27  
    1.28 +lemma [code func, code func del]:
    1.29 +  "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
    1.30 +
    1.31 +code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
    1.32 +  (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    1.33 +
    1.34  end