src/HOL/Inductive.thy
changeset 63863 d14e580c3b8f
parent 63588 d0e2bad67bd4
child 63976 c1a481bb82d3
     1.1 --- a/src/HOL/Inductive.thy	Tue Sep 13 16:23:12 2016 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Sep 13 20:51:14 2016 +0200
     1.3 @@ -369,6 +369,15 @@
     1.4    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
     1.5    Collect_mono in_mono vimage_mono
     1.6  
     1.7 +lemma le_rel_bool_arg_iff: "X \<le> Y \<longleftrightarrow> X False \<le> Y False \<and> X True \<le> Y True"
     1.8 +  unfolding le_fun_def le_bool_def using bool_induct by auto
     1.9 +
    1.10 +lemma imp_conj_iff: "((P \<longrightarrow> Q) \<and> P) = (P \<and> Q)"
    1.11 +  by blast
    1.12 +
    1.13 +lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
    1.14 +  by auto
    1.15 +
    1.16  ML_file "Tools/inductive.ML"
    1.17  
    1.18  lemmas [mono] =