src/HOL/Presburger.thy
changeset 24404 317b207bc1ab
parent 24094 6db35c14146d
child 24993 92dfacb32053
     1.1 --- a/src/HOL/Presburger.thy	Wed Aug 22 17:13:41 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Aug 22 17:13:42 2007 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4  
     1.5  subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
     1.6  
     1.7 +
     1.8  lemma minf:
     1.9    "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    1.10       \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"