# HG changeset patch
# User nipkow
# Date 1185479281 -7200
# Node ID f30b7a65282370651bf56cb3c029e6304f880e9c
# Parent  bf352c4c499bd8d30a704e968d8c9d9a36784400
fixed broken proof

diff -r bf352c4c499b -r f30b7a652823 src/HOL/Complex/ex/MIR.thy
--- a/src/HOL/Complex/ex/MIR.thy	Wed Jul 25 22:20:54 2007 +0200
+++ b/src/HOL/Complex/ex/MIR.thy	Thu Jul 26 21:48:01 2007 +0200
@@ -2140,17 +2140,17 @@
   let ?d = "\<delta> (And p q)"
   from prems ilcm_pos have dp: "?d >0" by simp
   have d1: "\<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
-  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
-  from th th' dp show ?case by simp 
+   hence th: "d\<delta> p ?d" using delta_mono prems by(auto simp del: dvd_ilcm_self1)
+  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)
+  from th th' dp show ?case by simp
 next
   case (2 p q)  
   let ?d = "\<delta> (And p q)"
   from prems ilcm_pos have dp: "?d >0" by simp
-  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
-  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
-  from th th' dp show ?case by simp 
+  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)
+  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)
+  from th th' dp show ?case by simp
 qed simp_all