src/HOL/String.thy
changeset 52365 95186e6e4bf4
parent 51717 9e7d1c139569
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/String.thy	Mon Jun 10 20:43:17 2013 +0200
     1.2 +++ b/src/HOL/String.thy	Tue Jun 11 21:07:53 2013 +0200
     1.3 @@ -382,6 +382,11 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma [code nbe]:
     1.8 +  fixes s :: "String.literal"
     1.9 +  shows "HOL.equal s s \<longleftrightarrow> True"
    1.10 +  by (simp add: equal)
    1.11 +
    1.12  lemma STR_inject' [simp]:
    1.13    "STR xs = STR ys \<longleftrightarrow> xs = ys"
    1.14    by (simp add: STR_inject)