src/HOL/BNF_Fixpoint_Base.thy
changeset 62335 e85c42f4f30a
parent 62325 7e4d31eefe60
child 62905 52c5a25e0c96
     1.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Tue Feb 16 22:28:19 2016 +0100
     1.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Wed Feb 17 17:08:36 2016 +0100
     1.3 @@ -236,6 +236,12 @@
     1.4  lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
     1.5    unfolding rel_fun_def by simp
     1.6  
     1.7 +lemma eq_onp_live_step: "x = y \<Longrightarrow> eq_onp P a a \<and> x \<longleftrightarrow> P a \<and> y"
     1.8 +  by (simp only: eq_onp_same_args)
     1.9 +
    1.10 +lemma top_conj: "top x \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
    1.11 +  by blast+
    1.12 +
    1.13  ML_file "Tools/BNF/bnf_fp_util.ML"
    1.14  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    1.15  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"