diff -r 8ebc8f530ab4 -r 342d74ca8815 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sat Jun 18 00:33:27 2005 +0200
+++ b/src/HOLCF/Fixrec.thy	Sat Jun 18 00:38:18 2005 +0200
@@ -179,10 +179,16 @@
 lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
 by simp
 
+text {* lemma for proving rewrite rules *}
+
+lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
+by simp
+
 ML {*
 val cpair_equalI = thm "cpair_equalI";
 val cpair_eqD1 = thm "cpair_eqD1";
 val cpair_eqD2 = thm "cpair_eqD2";
+val ssubst_lhs = thm "ssubst_lhs";
 *}
 
 subsection {* Intitializing the fixrec package *}