# HG changeset patch
# User wenzelm
# Date 881338825 -3600
# Node ID b9852572af0f36a9258efcdf9249bc4816d29fc5
# Parent  8755cdbbf6b36e112581104cb449d2c1fbd50303
adapted proofs to cope with simprocs nat_cancel;

diff -r 8755cdbbf6b3 -r b9852572af0f src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Dec 05 17:19:38 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Dec 05 17:20:25 1997 +0100
@@ -53,7 +53,8 @@
          "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"];
 
 
-(* Arithmetic *)
+(* Arithmetic *)	(* FIXME cleanup *)
+
 goal Arith.thy "n ~= 0 --> Suc(m+pred(n)) = m+n";
   by (nat_ind_tac "n" 1);
   by (REPEAT(Simp_tac 1));
@@ -131,7 +132,7 @@
   by (dtac (less_eq_add_cong RS mp) 1);
   by (cut_facts_tac [le_refl] 1);
   by (dres_inst_tac [("P","x<=x")] mp 1);by (assume_tac 1);
-  by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
+  by (asm_full_simp_tac (simpset() delsimprocs nat_cancel addsimps [add_commute]) 1);
   by (rtac impI 1);
   by (etac le_trans 1);
   by (assume_tac 1);