src/HOL/Tools/refute.ML
changeset 38786 e46e7a9cb622
parent 38553 56965d8e4e11
child 38795 848be46708dc
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -650,7 +650,7 @@
     1.4        | Const (@{const_name "op ="}, _) => t
     1.5        | Const (@{const_name "op &"}, _) => t
     1.6        | Const (@{const_name "op |"}, _) => t
     1.7 -      | Const (@{const_name "op -->"}, _) => t
     1.8 +      | Const (@{const_name HOL.implies}, _) => t
     1.9        (* sets *)
    1.10        | Const (@{const_name Collect}, _) => t
    1.11        | Const (@{const_name Set.member}, _) => t
    1.12 @@ -826,7 +826,7 @@
    1.13        | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
    1.14        | Const (@{const_name "op &"}, _) => axs
    1.15        | Const (@{const_name "op |"}, _) => axs
    1.16 -      | Const (@{const_name "op -->"}, _) => axs
    1.17 +      | Const (@{const_name HOL.implies}, _) => axs
    1.18        (* sets *)
    1.19        | Const (@{const_name Collect}, T) => collect_type_axioms T axs
    1.20        | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
    1.21 @@ -1895,7 +1895,7 @@
    1.22        (* this would make "undef" propagate, even for formulae like *)
    1.23        (* "True | undef":                                           *)
    1.24        (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
    1.25 -    | Const (@{const_name "op -->"}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
    1.26 +    | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
    1.27        (* 3-valued logic *)
    1.28        let
    1.29          val (i1, m1, a1) = interpret thy model args t1
    1.30 @@ -1905,9 +1905,9 @@
    1.31        in
    1.32          SOME (Leaf [fmTrue, fmFalse], m2, a2)
    1.33        end
    1.34 -    | Const (@{const_name "op -->"}, _) $ t1 =>
    1.35 +    | Const (@{const_name HOL.implies}, _) $ t1 =>
    1.36        SOME (interpret thy model args (eta_expand t 1))
    1.37 -    | Const (@{const_name "op -->"}, _) =>
    1.38 +    | Const (@{const_name HOL.implies}, _) =>
    1.39        SOME (interpret thy model args (eta_expand t 2))
    1.40        (* this would make "undef" propagate, even for formulae like *)
    1.41        (* "False --> undef":                                        *)