src/HOL/BNF_FP_Base.thy
changeset 57489 8f0ba9f2d10f
parent 57471 11cd462e31ec
child 57525 f9dd8a33f820
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Jul 02 13:23:11 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Wed Jul 02 17:01:49 2014 +0200
     1.3 @@ -187,6 +187,9 @@
     1.4  lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
     1.5    by (simp add: inj_on_def)
     1.6  
     1.7 +lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
     1.8 +  by simp
     1.9 +
    1.10  ML_file "Tools/BNF/bnf_fp_util.ML"
    1.11  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    1.12  ML_file "Tools/BNF/bnf_lfp_size.ML"