1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Nov 20 11:10:05 2013 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Nov 20 11:12:35 2013 +0100
     1.3 @@ -94,6 +94,30 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation String.literal :: linorder
     1.8 +begin
     1.9 +
    1.10 +lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
    1.11 +lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
    1.12 +
    1.13 +instance
    1.14 +proof -
    1.15 +  interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
    1.16 +    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
    1.17 +  show "PROP ?thesis"
    1.18 +    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
    1.19 +qed
    1.20 +
    1.21 +end
    1.22 +
    1.23 +lemma less_literal_code [code]: 
    1.24 +  "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
    1.25 +by(simp add: less_literal.rep_eq fun_eq_iff)
    1.26 +
    1.27 +lemma less_eq_literal_code [code]:
    1.28 +  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
    1.29 +by(simp add: less_eq_literal.rep_eq fun_eq_iff)
    1.30 +
    1.31  text {* Legacy aliasses *}
    1.32  
    1.33  lemmas nibble_less_eq_def = less_eq_nibble_def