tuned;

--- a/src/HOL/Presburger.thy	Wed Aug 22 17:13:41 2007 +0200
+++ b/src/HOL/Presburger.thy	Wed Aug 22 17:13:42 2007 +0200
@@ -18,6 +18,7 @@
 
 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
 
+
 lemma minf:
   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
      \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"