src/HOL/arith_data.ML

--- a/src/HOL/arith_data.ML	Tue Feb 26 12:51:40 2002 +0100
+++ b/src/HOL/arith_data.ML	Tue Feb 26 13:37:48 2002 +0100
@@ -368,8 +368,6 @@
 *)
 val add_rules =
  [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
-  add_not_0_if_left_not_0,add_not_0_if_right_not_0,
-  add_not_0_if_left_not_0 RS not_sym,add_not_0_if_right_not_0 RS not_sym,
   One_nat_def];
 
 val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s