equal
deleted
inserted
replaced
32 char |
32 char |
33 |
33 |
34 code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
34 code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool" |
35 (SML "!((_ : char) = _)") |
35 (SML "!((_ : char) = _)") |
36 (OCaml "!((_ : char) = _)") |
36 (OCaml "!((_ : char) = _)") |
37 (Haskell infixl 4 "==") |
37 (Haskell infix 4 "==") |
38 (Scala infixl 5 "==") |
38 (Scala infixl 5 "==") |
39 |
39 |
40 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" |
40 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" |
41 (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
41 (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") |
42 |
42 |