src/HOL/BNF/BNF_GFP.thy

--- a/src/HOL/BNF/BNF_GFP.thy	Thu May 09 03:58:28 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Thu May 09 20:44:37 2013 +0200
@@ -335,6 +335,12 @@
 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
 by simp
 
+lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
+by auto
+
+lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
+by blast
+
 ML_file "Tools/bnf_gfp_util.ML"
 ML_file "Tools/bnf_gfp_tactics.ML"
 ML_file "Tools/bnf_gfp.ML"