Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
implement comparisons on String.literal by target-language comparisons
authorAndreas Lochbihler
Wed, 20 Nov 2013 11:59:33 +0100
changeset 54596 368c70ee1f46
parent 54595 a2eeeb335a48
child 54597 4af7c82463d3
implement comparisons on String.literal by target-language comparisons
src/HOL/Library/Code_Char.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Code_Char.thy	Wed Nov 20 11:12:35 2013 +0100
+++ b/src/HOL/Library/Code_Char.thy	Wed Nov 20 11:59:33 2013 +0100
@@ -97,6 +97,18 @@
     and (Haskell) infix 4 "<"
     and (Scala) infixl 4 "<"
     and (Eval) infixl 6 "<"
+|  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+    (SML) "!((_ : string) <= _)"
+    and (OCaml) "!((_ : string) <= _)"
+    and (Haskell) infix 4 "<="
+    and (Scala) infixl 4 "<="
+    and (Eval) infixl 6 "<="
+| constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+    (SML) "!((_ : string) < _)"
+    and (OCaml) "!((_ : string) < _)"
+    and (Haskell) infix 4 "<"
+    and (Scala) infixl 4 "<"
+    and (Eval) infixl 6 "<"
 
 end
isabelle