diff -r cdf586d56b8a -r f1f7964ed05c src/FOL/simpdata.ML
--- 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",