src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -2954,8 +2954,8 @@
     1.4  fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
     1.5  val brT = [bT, bT] ---> bT;
     1.6  val nott = @{term "Not"};
     1.7 -val conjt = @{term "op &"};
     1.8 -val disjt = @{term "op |"};
     1.9 +val conjt = @{term HOL.conj};
    1.10 +val disjt = @{term HOL.disj};
    1.11  val impt = @{term HOL.implies};
    1.12  val ifft = @{term "op = :: bool => _"}
    1.13  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    1.14 @@ -3018,8 +3018,8 @@
    1.15      Const(@{const_name True},_) => @{code T}
    1.16    | Const(@{const_name False},_) => @{code F}
    1.17    | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
    1.18 -  | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    1.19 -  | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    1.20 +  | Const(@{const_name HOL.conj},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    1.21 +  | Const(@{const_name HOL.disj},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    1.22    | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    1.23    | Const(@{const_name "op ="},ty)$p$q => 
    1.24         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)