src/HOL/Decision_Procs/MIR.thy
changeset 31730 d74830dc3e4a
parent 31706 1db0c8f235fb
child 31952 40501bb2d57c
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Jun 20 01:53:39 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Jun 20 13:34:54 2009 +0200
     1.3 @@ -2129,18 +2129,18 @@
     1.4    from prems int_lcm_pos have dp: "?d >0" by simp
     1.5    have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 
     1.6     hence th: "d\<delta> p ?d" 
     1.7 -     using delta_mono prems by (auto simp del: int_lcm_dvd1)
     1.8 +     using delta_mono prems by(simp only: iszlfm.simps) blast
     1.9    have "\<delta> q dvd \<delta> (And p q)" using prems  by simp 
    1.10 -  hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: int_lcm_dvd2)
    1.11 +  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast
    1.12    from th th' dp show ?case by simp 
    1.13  next
    1.14    case (2 p q)  
    1.15    let ?d = "\<delta> (And p q)"
    1.16    from prems int_lcm_pos have dp: "?d >0" by simp
    1.17    have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 
    1.18 -    by (auto simp del: int_lcm_dvd1)
    1.19 -  have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: int_lcm_dvd2)
    1.20 -  from th th' dp show ?case by simp 
    1.21 +    by(simp only: iszlfm.simps) blast
    1.22 +  have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast
    1.23 +  from th th' dp show ?case by simp
    1.24  qed simp_all
    1.25  
    1.26