| changeset 12825 | f1f7964ed05c |
| parent 12765 | fb3f9887d0b7 |
| child 13149 | 773657d466cb |
--- a/src/FOL/simpdata.ML Mon Jan 21 14:47:47 2002 +0100 +++ b/src/FOL/simpdata.ML Mon Jan 21 14:47:55 2002 +0100 @@ -352,7 +352,7 @@ bind_thms ("cla_simps", [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, - not_all, not_ex, cases_simp] @ + not_imp, not_all, not_ex, cases_simp] @ map prove_fun ["~(P&Q) <-> ~P | ~Q", "P | ~P", "~P | P",