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));