--- a/src/HOL/BNF_Def.thy Wed Feb 17 11:39:26 2016 +0100
+++ b/src/HOL/BNF_Def.thy Wed Feb 17 15:18:06 2016 +0100
@@ -265,6 +265,10 @@
lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)"
by auto
+lemma rel_fun_Collect_case_prodD:
+ "rel_fun A B f g \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f o fst) x) ((g o snd) x)"
+ unfolding rel_fun_def by auto
+
ML_file "Tools/BNF/bnf_util.ML"
ML_file "Tools/BNF/bnf_tactics.ML"
ML_file "Tools/BNF/bnf_def_tactics.ML"