1.1 --- a/src/HOL/Complex/ex/MIR.thy	Wed Jul 25 22:20:54 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/MIR.thy	Thu Jul 26 21:48:01 2007 +0200
     1.3 @@ -2140,17 +2140,17 @@
     1.4    let ?d = "\<delta> (And p q)"
     1.5    from prems ilcm_pos have dp: "?d >0" by simp
     1.6    have d1: "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp 
     1.7 -   hence th: "d\<delta> p ?d" using delta_mono prems by auto
     1.8 -  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp 
     1.9 -  hence th': "d\<delta> q ?d" using delta_mono prems by auto
    1.10 -  from th th' dp show ?case by simp 
    1.11 +   hence th: "d\<delta> p ?d" using delta_mono prems by(auto simp del: dvd_ilcm_self1)
    1.12 +  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by(simp)
    1.13 +  hence th': "d\<delta> q ?d" using delta_mono prems by(auto simp del: dvd_ilcm_self2)
    1.14 +  from th th' dp show ?case by simp
    1.15  next
    1.16    case (2 p q)  
    1.17    let ?d = "\<delta> (And p q)"
    1.18    from prems ilcm_pos have dp: "?d >0" by simp
    1.19 -  have "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp hence th: "d\<delta> p ?d" using delta_mono prems by auto
    1.20 -  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp hence th': "d\<delta> q ?d" using delta_mono prems by auto
    1.21 -  from th th' dp show ?case by simp 
    1.22 +  have "\<delta> p dvd \<delta> (And p q)" using prems ilcm_dvd1 by simp hence th: "d\<delta> p ?d" using delta_mono prems by(auto simp del: dvd_ilcm_self1)
    1.23 +  have "\<delta> q dvd \<delta> (And p q)" using prems ilcm_dvd2 by simp hence th': "d\<delta> q ?d" using delta_mono prems by(auto simp del: dvd_ilcm_self2)
    1.24 +  from th th' dp show ?case by simp
    1.25  qed simp_all
    1.26  
    1.27