# HG changeset patch
# User Andreas Lochbihler
# Date 1385546084 -3600
# Node ID 17d76426c7da14ed281f7998b98a58e3c32ebd54
# Parent  33a68b7f2736ba5303c5e646f16cdfb4cceb699c
revert 4af7c82463d3 and document type class problem in Haskell

diff -r 33a68b7f2736 -r 17d76426c7da src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Wed Nov 27 10:43:51 2013 +0100
+++ b/src/HOL/Library/Code_Char.thy	Wed Nov 27 10:54:44 2013 +0100
@@ -100,6 +100,9 @@
 |  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
     (SML) "!((_ : string) <= _)"
     and (OCaml) "!((_ : string) <= _)"
+    -- {* Order operations for @{typ String.literal} work in Haskell only 
+          if no type class instance needs to be generated, because String = [Char] in Haskell
+          and @{typ "char list"} need not have the same order as @{typ String.literal}. *}
     and (Haskell) infix 4 "<="
     and (Scala) infixl 4 "<="
     and (Eval) infixl 6 "<="
diff -r 33a68b7f2736 -r 17d76426c7da src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Wed Nov 27 10:43:51 2013 +0100
+++ b/src/HOL/Library/List_lexord.thy	Wed Nov 27 10:54:44 2013 +0100
@@ -118,6 +118,4 @@
   "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
   by simp_all
 
-code_printing class_instance String.literal :: ord \<rightharpoonup> (Haskell) -
-
 end