# HG changeset patch
# User Andreas Lochbihler
# Date 1384945173 -3600
# Node ID 368c70ee1f46abf636bba20d458629757c40610e
# Parent  a2eeeb335a48dafb81d415a3410237a74ddc9788
implement comparisons on String.literal by target-language comparisons

diff -r a2eeeb335a48 -r 368c70ee1f46 src/HOL/Library/Code_Char.thy
--- 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