# HG changeset patch
# User chaieb
# Date 1114595360 -7200
# Node ID 7bc8b9683224b349ff5ca2cc6e33f7e2ebac27ee
# Parent  d9f0c8580c0cbe53df0286c021122ea246cdee51
bug in plusinf and mininf for the oracle fixed.

diff -r d9f0c8580c0c -r 7bc8b9683224 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Wed Apr 27 06:03:35 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Wed Apr 27 11:49:20 2005 +0200
@@ -323,8 +323,11 @@
 	 				 else fm 
  
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
-  )) => 
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.false_const else HOLogic.true_const 
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
+	          else error "minusinf : term not in normal form!!!"
+	else fm
 	 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) 
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) 
@@ -341,8 +344,11 @@
 	 				 else fm
 
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
-  )) =>
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.true_const else HOLogic.false_const
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+	     else error "plusinf : term not in normal form!!!"
+	else fm 
 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p)
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q)
diff -r d9f0c8580c0c -r 7bc8b9683224 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Apr 27 06:03:35 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Apr 27 11:49:20 2005 +0200
@@ -323,8 +323,11 @@
 	 				 else fm 
  
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
-  )) => 
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.false_const else HOLogic.true_const 
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
+	          else error "minusinf : term not in normal form!!!"
+	else fm
 	 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) 
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) 
@@ -341,8 +344,11 @@
 	 				 else fm
 
   |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
-  )) =>
-        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.true_const else HOLogic.false_const
+  )) => if (x = y) 
+	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
+	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
+	     else error "plusinf : term not in normal form!!!"
+	else fm 
 
   |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p)
   |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q)