1.1 --- a/src/HOL/Integ/cooper_dec.ML	Wed Apr 27 06:03:35 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Wed Apr 27 11:49:20 2005 +0200
     1.3 @@ -323,8 +323,11 @@
     1.4  	 				 else fm 
     1.5   
     1.6    |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
     1.7 -  )) => 
     1.8 -        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.false_const else HOLogic.true_const 
     1.9 +  )) => if (x = y) 
    1.10 +	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
    1.11 +	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
    1.12 +	          else error "minusinf : term not in normal form!!!"
    1.13 +	else fm
    1.14  	 
    1.15    |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) 
    1.16    |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) 
    1.17 @@ -341,8 +344,11 @@
    1.18  	 				 else fm
    1.19  
    1.20    |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
    1.21 -  )) =>
    1.22 -        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.true_const else HOLogic.false_const
    1.23 +  )) => if (x = y) 
    1.24 +	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
    1.25 +	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
    1.26 +	     else error "plusinf : term not in normal form!!!"
    1.27 +	else fm 
    1.28  
    1.29    |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p)
    1.30    |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q)

     2.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Apr 27 06:03:35 2005 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Apr 27 11:49:20 2005 +0200
     2.3 @@ -323,8 +323,11 @@
     2.4  	 				 else fm 
     2.5   
     2.6    |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z 
     2.7 -  )) => 
     2.8 -        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.false_const else HOLogic.true_const 
     2.9 +  )) => if (x = y) 
    2.10 +	then if (pm1 = one) andalso (c = zero) then HOLogic.false_const 
    2.11 +	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.true_const 
    2.12 +	          else error "minusinf : term not in normal form!!!"
    2.13 +	else fm
    2.14  	 
    2.15    |(Const ("Not", _) $ p) => HOLogic.Not $ (minusinf x p) 
    2.16    |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (minusinf x p) $ (minusinf x q) 
    2.17 @@ -341,8 +344,11 @@
    2.18  	 				 else fm
    2.19  
    2.20    |(Const("op <",_) $ c $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z
    2.21 -  )) =>
    2.22 -        if (x =y) andalso (pm1 = one) andalso (c = zero) then HOLogic.true_const else HOLogic.false_const
    2.23 +  )) => if (x = y) 
    2.24 +	then if (pm1 = one) andalso (c = zero) then HOLogic.true_const 
    2.25 +	     else if (dest_numeral pm1 = ~1) andalso (c = zero) then HOLogic.false_const
    2.26 +	     else error "plusinf : term not in normal form!!!"
    2.27 +	else fm 
    2.28  
    2.29    |(Const ("Not", _) $ p) => HOLogic.Not $ (plusinf x p)
    2.30    |(Const ("op &",_) $ p $ q) => HOLogic.conj $ (plusinf x p) $ (plusinf x q)