--- a/src/HOL/String.thy Wed Nov 20 10:59:12 2013 +0100
+++ b/src/HOL/String.thy Wed Nov 20 11:10:05 2013 +0100
@@ -358,6 +358,8 @@
typedef literal = "UNIV :: string set"
morphisms explode STR ..
+setup_lifting (no_code) type_definition_literal
+
instantiation literal :: size
begin
@@ -372,16 +374,14 @@
instantiation literal :: equal
begin
-definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
-where
- "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
+lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
-instance
-proof
-qed (auto simp add: equal_literal_def explode_inject)
+instance by intro_classes (transfer, simp)
end
+declare equal_literal.rep_eq[code]
+
lemma [code nbe]:
fixes s :: "String.literal"
shows "HOL.equal s s \<longleftrightarrow> True"
@@ -391,7 +391,6 @@
"STR xs = STR ys \<longleftrightarrow> xs = ys"
by (simp add: STR_inject)
-
subsection {* Code generator *}
ML_file "Tools/string_code.ML"