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