src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 35084 e25eedfc15ce
parent 35045 a77d200e6503
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 08:49:26 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 08:49:26 2010 +0100
     1.3 @@ -2946,7 +2946,7 @@
     1.4  fun num rT x = HOLogic.mk_number rT x;
     1.5  fun rrelT rT = [rT,rT] ---> rT;
     1.6  fun rrT rT = [rT, rT] ---> bT;
     1.7 -fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
     1.8 +fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
     1.9  fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
    1.10  fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
    1.11  fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
    1.12 @@ -2974,7 +2974,7 @@
    1.13   | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    1.14   | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
    1.15   | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
    1.16 - | Const(@{const_name Algebras.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.17 + | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.18   | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) 
    1.19           handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
    1.20