# HG changeset patch
# User chaieb
# Date 1187795622 -7200
# Node ID 317b207bc1ab8282f535fb50b9edad0f583a0f0c
# Parent  b7c3ee2ca184c838ed0da080aa2684fa7b912735
tuned;

diff -r b7c3ee2ca184 -r 317b207bc1ab src/HOL/Presburger.thy
--- 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)"