1.1 --- a/src/HOL/String.thy Wed Nov 20 10:59:12 2013 +0100
1.2 +++ b/src/HOL/String.thy Wed Nov 20 11:10:05 2013 +0100
1.3 @@ -358,6 +358,8 @@
1.4 typedef literal = "UNIV :: string set"
1.5 morphisms explode STR ..
1.6
1.7 +setup_lifting (no_code) type_definition_literal
1.8 +
1.9 instantiation literal :: size
1.10 begin
1.11
1.12 @@ -372,16 +374,14 @@
1.13 instantiation literal :: equal
1.14 begin
1.15
1.16 -definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
1.17 -where
1.18 - "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
1.19 +lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
1.20
1.21 -instance
1.22 -proof
1.23 -qed (auto simp add: equal_literal_def explode_inject)
1.24 +instance by intro_classes (transfer, simp)
1.25
1.26 end
1.27
1.28 +declare equal_literal.rep_eq[code]
1.29 +
1.30 lemma [code nbe]:
1.31 fixes s :: "String.literal"
1.32 shows "HOL.equal s s \<longleftrightarrow> True"
1.33 @@ -391,7 +391,6 @@
1.34 "STR xs = STR ys \<longleftrightarrow> xs = ys"
1.35 by (simp add: STR_inject)
1.36
1.37 -
1.38 subsection {* Code generator *}
1.39
1.40 ML_file "Tools/string_code.ML"