make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
--- a/src/HOL/Library/Char_ord.thy Tue Feb 11 12:08:44 2014 +0100
+++ b/src/HOL/Library/Char_ord.thy Wed Feb 12 08:56:38 2014 +0100
@@ -97,6 +97,7 @@
instantiation String.literal :: linorder
begin
+context includes literal.lifting begin
lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
@@ -109,6 +110,7 @@
qed
end
+end
lemma less_literal_code [code]:
"op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
@@ -118,6 +120,9 @@
"op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
by(simp add: less_eq_literal.rep_eq fun_eq_iff)
+lifting_update literal.lifting
+lifting_forget literal.lifting
+
text {* Legacy aliasses *}
lemmas nibble_less_eq_def = less_eq_nibble_def
--- a/src/HOL/String.thy Tue Feb 11 12:08:44 2014 +0100
+++ b/src/HOL/String.thy Wed Feb 12 08:56:38 2014 +0100
@@ -391,6 +391,9 @@
"STR xs = STR ys \<longleftrightarrow> xs = ys"
by (simp add: STR_inject)
+lifting_update literal.lifting
+lifting_forget literal.lifting
+
subsection {* Code generator *}
ML_file "Tools/string_code.ML"