src/HOL/Library/Char_ord.thy
changeset 55426 90f2ceed2828
parent 54863 82acc20ded73
child 57437 0baf08c075b9
     1.1 --- a/src/HOL/Library/Char_ord.thy	Tue Feb 11 12:08:44 2014 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Feb 12 08:56:38 2014 +0100
     1.3 @@ -97,6 +97,7 @@
     1.4  instantiation String.literal :: linorder
     1.5  begin
     1.6  
     1.7 +context includes literal.lifting begin
     1.8  lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
     1.9  lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
    1.10  
    1.11 @@ -109,6 +110,7 @@
    1.12  qed
    1.13  
    1.14  end
    1.15 +end
    1.16  
    1.17  lemma less_literal_code [code]: 
    1.18    "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
    1.19 @@ -118,6 +120,9 @@
    1.20    "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
    1.21  by(simp add: less_eq_literal.rep_eq fun_eq_iff)
    1.22  
    1.23 +lifting_update literal.lifting
    1.24 +lifting_forget literal.lifting
    1.25 +
    1.26  text {* Legacy aliasses *}
    1.27  
    1.28  lemmas nibble_less_eq_def = less_eq_nibble_def