# HG changeset patch
# User nipkow
# Date 1185379849 -7200
# Node ID aaff3bc5ec28736c44b2ab2d9e4e86c613bcace3
# Parent  79dc793bec4344013278370cb091fcc4d68736f0
fixed broken proof

diff -r 79dc793bec43 -r aaff3bc5ec28 src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Wed Jul 25 18:10:28 2007 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Jul 25 18:10:49 2007 +0200
@@ -1080,18 +1080,20 @@
   case (1 p q) 
   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 
+  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(3-4) by(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(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(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(simp del:dvd_ilcm_self2)
+  from th th' dp show ?case by simp
 qed simp_all