src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 35092 cfe605c54e50
parent 35084 e25eedfc15ce
child 35267 8dfd816713c6
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -2958,8 +2958,8 @@
     1.4  val disjt = @{term "op |"};
     1.5  val impt = @{term "op -->"};
     1.6  val ifft = @{term "op = :: bool => _"}
     1.7 -fun llt rT = Const(@{const_name Algebras.less},rrT rT);
     1.8 -fun lle rT = Const(@{const_name Algebras.less},rrT rT);
     1.9 +fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    1.10 +fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    1.11  fun eqt rT = Const("op =",rrT rT);
    1.12  fun rz rT = Const(@{const_name Algebras.zero},rT);
    1.13  
    1.14 @@ -3024,9 +3024,9 @@
    1.15    | Const("op =",ty)$p$q => 
    1.16         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
    1.17         else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    1.18 -  | Const(@{const_name Algebras.less},_)$p$q => 
    1.19 +  | Const(@{const_name Orderings.less},_)$p$q => 
    1.20          @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    1.21 -  | Const(@{const_name Algebras.less_eq},_)$p$q => 
    1.22 +  | Const(@{const_name Orderings.less_eq},_)$p$q => 
    1.23          @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    1.24    | Const("Ex",_)$Abs(xn,xT,p) => 
    1.25       let val (xn', p') =  variant_abs (xn,xT,p)