src/HOL/BNF_LFP.thy
changeset 55851 3d40cf74726c
parent 55811 aa1acc25126b
child 55856 bddaada24074
--- a/src/HOL/BNF_LFP.thy	Mon Mar 03 03:13:45 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:19 2014 +0100
@@ -251,10 +251,10 @@
   unfolding vimage2p_def by auto
 
 lemma id_transfer: "fun_rel A A id id"
-unfolding fun_rel_def by simp
+  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
+  by (rule ssubst)
 
 ML_file "Tools/BNF/bnf_lfp_util.ML"
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"