# HG changeset patch # User Andreas Lochbihler # Date 1384945872 -3600 # Node ID 4af7c82463d36cf54e195afbd8cf74c2b3c4d1f3 # Parent 368c70ee1f46abf636bba20d458629757c40610e no ord instance for String.literal in Haskell when list is also ordered lexicographically diff -r 368c70ee1f46 -r 4af7c82463d3 src/HOL/Library/List_lexord.thy --- a/src/HOL/Library/List_lexord.thy Wed Nov 20 11:59:33 2013 +0100 +++ b/src/HOL/Library/List_lexord.thy Wed Nov 20 12:11:12 2013 +0100 @@ -118,4 +118,6 @@ "(x\'a\{equal, order}) # xs \ y # ys \ x < y \ x = y \ xs \ ys" by simp_all +code_printing class_instance String.literal :: ord \ (Haskell) - + end