# HG changeset patch
# User Andreas Lochbihler
# Date 1384942205 -3600
# Node ID a2d1522cdd54ac0b34233d5c2c4c1252c065c485
# Parent  8c0a27b9c1bd31e5ded4fed9b5e93cb3582e9e99
setup lifting/transfer for String.literal

diff -r 8c0a27b9c1bd -r a2d1522cdd54 src/HOL/String.thy
--- 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"