src/HOL/Tools/Qelim/presburger.ML
changeset 32603 e08fdd615333
parent 31790 05c92381363c
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 09:07:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Sep 18 09:07:50 2009 +0200
     1.3 @@ -52,18 +52,18 @@
     1.4  
     1.5  local
     1.6   fun isnum t = case t of 
     1.7 -   Const(@{const_name "HOL.zero"},_) => true
     1.8 - | Const(@{const_name "HOL.one"},_) => true
     1.9 +   Const(@{const_name HOL.zero},_) => true
    1.10 + | Const(@{const_name HOL.one},_) => true
    1.11   | @{term "Suc"}$s => isnum s
    1.12   | @{term "nat"}$s => isnum s
    1.13   | @{term "int"}$s => isnum s
    1.14 - | Const(@{const_name "HOL.uminus"},_)$s => isnum s
    1.15 - | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
    1.16 - | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
    1.17 - | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
    1.18 - | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
    1.19 - | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
    1.20 - | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
    1.21 + | Const(@{const_name HOL.uminus},_)$s => isnum s
    1.22 + | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
    1.23 + | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
    1.24 + | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
    1.25 + | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
    1.26 + | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
    1.27 + | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
    1.28   | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
    1.29  
    1.30   fun ty cts t =