# 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 \ True" + by (simp add: equal) + lemma STR_inject' [simp]: "STR xs = STR ys \ xs = ys" by (simp add: STR_inject)