--- a/src/FOL/simpdata.ML Fri Nov 25 00:01:04 1994 +0100
+++ b/src/FOL/simpdata.ML Fri Nov 25 00:02:37 1994 +0100
@@ -114,6 +114,7 @@
prove_goal FOL.thy s
(fn prems => [ (cut_facts_tac prems 1),
(Cla.fast_tac FOL_cs 1) ]));
+
val cla_rews = map prove_fun
["~(P&Q) <-> ~P | ~Q",
"P | ~P", "~P | P",