src/HOL/ex/svc_funcs.ML
changeset 19233 77ca20b0ed77
parent 17465 93fc1211603f
child 19277 f7602e74d948
     1.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Mar 10 12:28:38 2006 +0100
     1.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 10 15:33:48 2006 +0100
     1.3 @@ -154,16 +154,16 @@
     1.4        | lit (Const("0", _)) = 0
     1.5        | lit (Const("1", _)) = 1
     1.6      (*translation of a literal expression [no variables]*)
     1.7 -    fun litExp (Const("op +", T) $ x $ y) =
     1.8 +    fun litExp (Const("HOL.plus", T) $ x $ y) =
     1.9            if is_numeric_op T then (litExp x) + (litExp y)
    1.10            else fail t
    1.11 -      | litExp (Const("op -", T) $ x $ y) =
    1.12 +      | litExp (Const("HOL.minus", T) $ x $ y) =
    1.13            if is_numeric_op T then (litExp x) - (litExp y)
    1.14            else fail t
    1.15 -      | litExp (Const("op *", T) $ x $ y) =
    1.16 +      | litExp (Const("HOL.times", T) $ x $ y) =
    1.17            if is_numeric_op T then (litExp x) * (litExp y)
    1.18            else fail t
    1.19 -      | litExp (Const("uminus", T) $ x)   =
    1.20 +      | litExp (Const("HOL.uminus", T) $ x)   =
    1.21            if is_numeric_op T then ~(litExp x)
    1.22            else fail t
    1.23        | litExp t = lit t
    1.24 @@ -171,21 +171,21 @@
    1.25      (*translation of a real/rational expression*)
    1.26      fun suc t = Interp("+", [Int 1, t])
    1.27      fun tm (Const("Suc", T) $ x) = suc (tm x)
    1.28 -      | tm (Const("op +", T) $ x $ y) =
    1.29 +      | tm (Const("HOL.plus", T) $ x $ y) =
    1.30            if is_numeric_op T then Interp("+", [tm x, tm y])
    1.31            else fail t
    1.32 -      | tm (Const("op -", T) $ x $ y) =
    1.33 +      | tm (Const("HOL.minus", T) $ x $ y) =
    1.34            if is_numeric_op T then
    1.35                Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
    1.36            else fail t
    1.37 -      | tm (Const("op *", T) $ x $ y) =
    1.38 +      | tm (Const("HOL.times", T) $ x $ y) =
    1.39            if is_numeric_op T then Interp("*", [tm x, tm y])
    1.40            else fail t
    1.41        | tm (Const("RealDef.rinv", T) $ x) =
    1.42            if domain_type T = HOLogic.realT then
    1.43                Rat(1, litExp x)
    1.44            else fail t
    1.45 -      | tm (Const("uminus", T) $ x) =
    1.46 +      | tm (Const("HOL.uminus", T) $ x) =
    1.47            if is_numeric_op T then Interp("*", [Int ~1, tm x])
    1.48            else fail t
    1.49        | tm t = Int (lit t)