src/HOL/BNF_LFP.thy

--- a/src/HOL/BNF_LFP.thy	Wed Feb 26 17:14:23 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Wed Feb 26 23:09:29 2014 +0100
@@ -236,6 +236,9 @@
 lemma id_transfer: "fun_rel A A id id"
 unfolding fun_rel_def by simp
 
+lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
+  by simp
+
 ML_file "Tools/BNF/bnf_lfp_util.ML"
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"
 ML_file "Tools/BNF/bnf_lfp.ML"