src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 44064 5bce8ff0d9ae
parent 44013 5cfc1c36ae97
child 45499 849d697adf1e
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Aug 08 08:55:49 2011 -0700
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Aug 08 09:52:09 2011 -0700
     1.3 @@ -2856,7 +2856,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 Rings.divide},rrelT rT);
     1.8 +fun divt rT = Const(@{const_name Fields.divide},rrelT rT);
     1.9  fun timest rT = Const(@{const_name Groups.times},rrelT rT);
    1.10  fun plust rT = Const(@{const_name Groups.plus},rrelT rT);
    1.11  fun minust rT = Const(@{const_name Groups.minus},rrelT rT);
    1.12 @@ -2884,7 +2884,7 @@
    1.13   | Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    1.14   | Const(@{const_name Groups.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 Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.17 + | Const(@{const_name Fields.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