changeset 1758 | 60613b065e9b |
parent 1722 | bb326972ede6 |
child 1821 | bc506bcb9fe4 |
--- a/src/HOL/simpdata.ML Wed May 22 17:11:54 1996 +0200 +++ b/src/HOL/simpdata.ML Wed May 22 17:30:16 1996 +0200 @@ -192,6 +192,8 @@ prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))"; prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; +prove "ex_imp" "((? x. P x) --> Q) = (!x. P x --> Q)"; + qed_goal "if_cancel" HOL.thy "(if c then x else x) = x" (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);