src/HOL/simpdata.ML
changeset 1660 8cb42cd97579
parent 1655 5be64540f275
child 1722 bb326972ede6
     1.1 --- a/src/HOL/simpdata.ML	Wed Apr 17 11:46:10 1996 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Apr 17 17:59:58 1996 +0200
     1.3 @@ -181,6 +181,9 @@
     1.4  prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
     1.5  prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
     1.6  
     1.7 +prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))";
     1.8 +prove "not_ex"  "(~ (? x.P(x))) = (! x.~P(x))";
     1.9 +
    1.10  prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
    1.11  prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
    1.12