src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 38786 e46e7a9cb622
parent 38558 32ad17fe2b9c
child 38795 848be46708dc
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -2956,7 +2956,7 @@
     1.4  val nott = @{term "Not"};
     1.5  val conjt = @{term "op &"};
     1.6  val disjt = @{term "op |"};
     1.7 -val impt = @{term "op -->"};
     1.8 +val impt = @{term HOL.implies};
     1.9  val ifft = @{term "op = :: bool => _"}
    1.10  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    1.11  fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    1.12 @@ -3020,7 +3020,7 @@
    1.13    | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
    1.14    | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    1.15    | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    1.16 -  | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    1.17 +  | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    1.18    | Const(@{const_name "op ="},ty)$p$q => 
    1.19         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
    1.20         else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))