--- a/src/HOL/BNF_Fixpoint_Base.thy Wed Feb 17 17:08:03 2016 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy Wed Feb 17 17:08:36 2016 +0100
@@ -236,6 +236,12 @@
lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
unfolding rel_fun_def by simp
+lemma eq_onp_live_step: "x = y \<Longrightarrow> eq_onp P a a \<and> x \<longleftrightarrow> P a \<and> y"
+ by (simp only: eq_onp_same_args)
+
+lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
+ by blast+
+
ML_file "Tools/BNF/bnf_fp_util.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar.ML"