src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 38558 32ad17fe2b9c
parent 38549 d0385f2764d8
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 16:08:54 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 19 16:08:59 2010 +0200
     1.3 @@ -3015,9 +3015,9 @@
     1.4  
     1.5  fun fm_of_term m m' fm = 
     1.6   case fm of
     1.7 -    Const(@{const_name "True"},_) => @{code T}
     1.8 -  | Const(@{const_name "False"},_) => @{code F}
     1.9 -  | Const(@{const_name "Not"},_)$p => @{code NOT} (fm_of_term m m' p)
    1.10 +    Const(@{const_name True},_) => @{code T}
    1.11 +  | Const(@{const_name False},_) => @{code F}
    1.12 +  | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
    1.13    | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    1.14    | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    1.15    | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    1.16 @@ -3028,13 +3028,13 @@
    1.17          @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    1.18    | Const(@{const_name Orderings.less_eq},_)$p$q => 
    1.19          @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    1.20 -  | Const(@{const_name "Ex"},_)$Abs(xn,xT,p) => 
    1.21 +  | Const(@{const_name Ex},_)$Abs(xn,xT,p) => 
    1.22       let val (xn', p') =  variant_abs (xn,xT,p)
    1.23           val x = Free(xn',xT)
    1.24           fun incr i = i + 1
    1.25           val m0 = (x,0):: (map (apsnd incr) m)
    1.26        in @{code E} (fm_of_term m0 m' p') end
    1.27 -  | Const(@{const_name "All"},_)$Abs(xn,xT,p) => 
    1.28 +  | Const(@{const_name All},_)$Abs(xn,xT,p) => 
    1.29       let val (xn', p') =  variant_abs (xn,xT,p)
    1.30           val x = Free(xn',xT)
    1.31           fun incr i = i + 1
    1.32 @@ -3045,8 +3045,8 @@
    1.33  
    1.34  fun term_of_fm T m m' t = 
    1.35    case t of
    1.36 -    @{code T} => Const(@{const_name "True"},bT)
    1.37 -  | @{code F} => Const(@{const_name "False"},bT)
    1.38 +    @{code T} => Const(@{const_name True},bT)
    1.39 +  | @{code F} => Const(@{const_name False},bT)
    1.40    | @{code NOT} p => nott $ (term_of_fm T m m' p)
    1.41    | @{code And} (p,q) => conjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)
    1.42    | @{code Or} (p,q) => disjt $ (term_of_fm T m m' p) $ (term_of_fm T m m' q)