equal
deleted
inserted
replaced
6 header {* Code generation of pretty characters (and strings) *} |
6 header {* Code generation of pretty characters (and strings) *} |
7 |
7 |
8 theory Code_Char |
8 theory Code_Char |
9 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval" |
9 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval" |
10 begin |
10 begin |
11 |
|
12 declare char.recs [code func del] char.cases [code func del] |
|
13 |
11 |
14 code_type char |
12 code_type char |
15 (SML "char") |
13 (SML "char") |
16 (OCaml "char") |
14 (OCaml "char") |
17 (Haskell "Char") |
15 (Haskell "Char") |
33 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
31 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
34 (SML "!((_ : char) = _)") |
32 (SML "!((_ : char) = _)") |
35 (OCaml "!((_ : char) = _)") |
33 (OCaml "!((_ : char) = _)") |
36 (Haskell infixl 4 "==") |
34 (Haskell infixl 4 "==") |
37 |
35 |
38 lemma [code func, code func del]: |
|
39 "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" .. |
|
40 |
|
41 code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term" |
36 code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term" |
42 (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
37 (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
43 |
38 |
44 end |
39 end |