--- a/src/HOL/BNF/BNF_FP_Basic.thy Tue Aug 20 16:10:58 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Tue Aug 20 17:39:07 2013 +0200
@@ -147,6 +147,12 @@
"(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
unfolding fun_rel_def ..
+lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
+ by auto
+
+lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
+ by auto
+
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/bnf_fp_def_sugar.ML"