src/HOL/Decision_Procs/Cooper.thy

 proof (induct p rule: iszlfm.induct)
   case (1 p q) 
   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
 
 
 consts