src/HOL/simpdata.ML
changeset 8114 09a7a180cc99
parent 7711 4dae7a4fceaf
child 8473 2798d2f71ec2
     1.1 --- a/src/HOL/simpdata.ML	Fri Jan 07 11:04:15 2000 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Jan 07 11:06:03 2000 +0100
     1.3 @@ -232,8 +232,8 @@
     1.4  prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))";
     1.5  
     1.6  (*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*)
     1.7 -prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
     1.8 -prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
     1.9 +prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)";
    1.10 +prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)";
    1.11  
    1.12  prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
    1.13  prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";