# HG changeset patch
# User haftmann
# Date 1370977673 -7200
# Node ID 95186e6e4bf4bb502414246c16d3d3e83a14316b
# Parent  3bed446c305b6c2e77654092767fc36cb4eef6e0
reflexive nbe equation for equality on String.literal

diff -r 3bed446c305b -r 95186e6e4bf4 src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Jun 10 20:43:17 2013 +0200
+++ b/src/HOL/String.thy	Tue Jun 11 21:07:53 2013 +0200
@@ -382,6 +382,11 @@
 
 end
 
+lemma [code nbe]:
+  fixes s :: "String.literal"
+  shows "HOL.equal s s \<longleftrightarrow> True"
+  by (simp add: equal)
+
 lemma STR_inject' [simp]:
   "STR xs = STR ys \<longleftrightarrow> xs = ys"
   by (simp add: STR_inject)