adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);

--- a/src/HOL/Auth/Shared.ML	Fri Dec 05 17:13:46 1997 +0100
+++ b/src/HOL/Auth/Shared.ML	Fri Dec 05 17:14:36 1997 +0100
@@ -149,10 +149,6 @@
 by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym, 
 				     le_add2, le_add1, 
 				     le_eq_less_Suc RS sym]) 1);
-by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
-by (stac (le_eq_less_Suc RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 2);
-by (REPEAT (rtac le_add1 1));
 qed "Nonce_supply3";
 
 goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";

--- a/src/HOL/Induct/Mutil.ML	Fri Dec 05 17:13:46 1997 +0100
+++ b/src/HOL/Induct/Mutil.ML	Fri Dec 05 17:14:36 1997 +0100
@@ -149,9 +149,9 @@
 (*Requires a small simpset that won't move the Suc applications*)
 by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
 by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
-by (asm_simp_tac (simpset() addsimps add_ac) 2);
+by (asm_simp_tac (simpset() delsimprocs nat_cancel addsimps add_ac) 2);
 by (asm_full_simp_tac 
-    (simpset() addsimps [mod_less, tiling_domino_0_1 RS sym]) 1);
+    (simpset() delsimprocs nat_cancel addsimps [mod_less, tiling_domino_0_1 RS sym]) 1);
 by (rtac less_trans 1);
 by (REPEAT
     (rtac card_Diff 1 

--- a/src/HOL/Integ/Integ.ML	Fri Dec 05 17:13:46 1997 +0100
+++ b/src/HOL/Integ/Integ.ML	Fri Dec 05 17:14:36 1997 +0100
@@ -212,10 +212,6 @@
 by (etac subst 1);
 by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [diff_add_inverse,diff_add_0]) 1);
-by (rtac impI 1);
-by (asm_simp_tac (simpset() addsimps
-                  [diff_add_inverse, diff_add_0, diff_Suc_add_0,
-                   diff_Suc_add_inverse]) 1);
 qed "zmagnitude_congruent";
 
 (*Resolve th against the corresponding facts for zmagnitude*)
@@ -251,7 +247,6 @@
 (*The rest should be trivial, but rearranging terms is hard*)
 by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps add_ac) 1);
 qed "zadd_congruent2";
 
 (*Resolve th against the corresponding facts for zadd*)
@@ -614,11 +609,6 @@
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1);
-by (asm_full_simp_tac
- (simpset() delsimps [add_Suc_right] addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
-by (resolve_tac [less_not_refl2 RS notE] 1);
-by (etac sym 2);
-by (REPEAT (resolve_tac [lessI, trans_less_add2, less_SucI] 1));
 qed "zless_not_sym";
 
 (* [| n<m; m<n |] ==> R *)

--- a/src/HOL/MiniML/W.ML	Fri Dec 05 17:13:46 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Fri Dec 05 17:14:36 1997 +0100
@@ -388,13 +388,6 @@
 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
 qed_spec_mp "W_correct_lemma";
 
-goal Arith.thy "!!n::nat. ~ k+n < n";
-by (nat_ind_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-by (trans_tac 1);
-val not_add_less1 = result();
-Addsimps [not_add_less1];
-
 (* Completeness of W w.r.t. has_type *)
 goal thy
  "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \