equal
deleted
inserted
replaced
26 | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> |
26 | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> |
27 (SML) "!((_ : char) = _)" |
27 (SML) "!((_ : char) = _)" |
28 and (OCaml) "!((_ : char) = _)" |
28 and (OCaml) "!((_ : char) = _)" |
29 and (Haskell) infix 4 "==" |
29 and (Haskell) infix 4 "==" |
30 and (Scala) infixl 5 "==" |
30 and (Scala) infixl 5 "==" |
31 | constant "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" \<rightharpoonup> |
31 | constant "Code_Evaluation.term_of :: char \<Rightarrow> term" \<rightharpoonup> |
32 (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))" |
32 (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))" |
33 |
33 |
34 code_reserved SML |
34 code_reserved SML |
35 char |
35 char |
36 |
36 |