--- a/src/HOL/Decision_Procs/Cooper.thy Sat Jun 20 01:53:39 2009 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Sat Jun 20 13:34:54 2009 +0200
@@ -1106,18 +1106,18 @@
let ?d = "\<delta> (And p q)"
from prems int_lcm_pos have dp: "?d >0" by simp
have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
- hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:int_lcm_dvd1)
+ hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps)
have "\<delta> q dvd \<delta> (And p q)" using prems by simp
- hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:int_lcm_dvd2)
+ hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
from th th' dp show ?case by simp
next
case (2 p q)
let ?d = "\<delta> (And p q)"
from prems int_lcm_pos have dp: "?d >0" by simp
have "\<delta> p dvd \<delta> (And p q)" using prems by simp
- hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:int_lcm_dvd1)
+ hence th: "d\<delta> p ?d" using delta_mono prems by(simp only: iszlfm.simps)
have "\<delta> q dvd \<delta> (And p q)" using prems by simp
- hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:int_lcm_dvd2)
+ hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
from th th' dp show ?case by simp
qed simp_all