Addition of not_imp (which pushes negation into implication) as a default
simprule

--- a/src/HOL/WF_Rel.ML	Wed Jun 18 15:30:32 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Wed Jun 18 15:31:31 1997 +0200
@@ -129,13 +129,8 @@
  by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
  by(Blast_tac 1);
 be swap 1;
-by(Asm_full_simp_tac 1);
-be exE 1;
-be swap 1;
-br impI 1;
-be swap 1;
-be exE 1;
-by(rename_tac "x" 1);
+by (Asm_full_simp_tac 1);
+by (Step_tac 1);
 by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
  br allI 1;

--- a/src/HOL/simpdata.ML	Wed Jun 18 15:30:32 1997 +0200
+++ b/src/HOL/simpdata.ML	Wed Jun 18 15:31:31 1997 +0200
@@ -177,6 +177,7 @@
 
 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
+prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
 prove "not_iff" "(P~=Q) = (P = (~Q))";
 
 (*Avoids duplication of subgoals after expand_if, when the true and false 
@@ -301,13 +302,15 @@
 			    setSolver  unsafe_solver
 			    setmksimps (mksimps mksimps_pairs);
 
-val HOL_ss = HOL_basic_ss addsimps ([triv_forall_equality, (* prunes params *)
-				     if_True, if_False, if_cancel,
-				     o_apply, imp_disjL, conj_assoc, disj_assoc,
-				     de_Morgan_conj, de_Morgan_disj, 
-				     not_all, not_ex, cases_simp]
-				    @ ex_simps @ all_simps @ simp_thms)
-			  addcongs [imp_cong];
+val HOL_ss = 
+    HOL_basic_ss addsimps 
+     ([triv_forall_equality, (* prunes params *)
+       if_True, if_False, if_cancel,
+       o_apply, imp_disjL, conj_assoc, disj_assoc,
+       de_Morgan_conj, de_Morgan_disj, not_imp,
+       not_all, not_ex, cases_simp]
+     @ ex_simps @ all_simps @ simp_thms)
+     addcongs [imp_cong];
 
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)"