formerly unnamed infix impliciation now named HOL.implies
authorhaftmann
Thu Aug 26 20:51:17 2010 +0200 (2010-08-26)
changeset 38786e46e7a9cb622
parent 38776 95df565aceb7
child 38787 948c002d773b
formerly unnamed infix impliciation now named HOL.implies
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Boogie/Tools/boogie_tactics.ML
src/HOL/Boogie/Tools/boogie_vcs.ML
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/HOL.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Orderings.thy
src/HOL/Prolog/prolog.ML
src/HOL/Set.thy
src/HOL/TLA/Intensional.thy
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/qelim.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/simpdata.ML
src/HOL/ex/Meson_Test.thy
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -504,7 +504,7 @@
     1.4          in
     1.5            Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
     1.6          end) ||
     1.7 -      binexp "implies" (binop @{term "op -->"}) ||
     1.8 +      binexp "implies" (binop @{term HOL.implies}) ||
     1.9        scan_line "distinct" num :|-- scan_count exp >>
    1.10          (fn [] => @{term True}
    1.11            | ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||
     2.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Aug 26 13:44:50 2010 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Aug 26 20:51:17 2010 +0200
     2.3 @@ -53,7 +53,7 @@
     2.4    fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
     2.5      | explode_conj t = [t] 
     2.6  
     2.7 -  fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
     2.8 +  fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
     2.9      | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
    2.10      | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
    2.11      | splt (_, @{term True}) = []
     3.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Thu Aug 26 13:44:50 2010 +0200
     3.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Thu Aug 26 20:51:17 2010 +0200
     3.3 @@ -59,8 +59,8 @@
     3.4      fun vc_of @{term True} = NONE
     3.5        | vc_of (@{term assert_at} $ Free (n, _) $ t) =
     3.6            SOME (Assert ((n, t), True))
     3.7 -      | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
     3.8 -      | vc_of (@{term "op -->"} $ t $ u) =
     3.9 +      | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
    3.10 +      | vc_of (@{term HOL.implies} $ t $ u) =
    3.11            vc_of u |> Option.map (assume t)
    3.12        | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
    3.13            SOME (vc_of u |> the_default True |> assert (n, t))
    3.14 @@ -76,7 +76,7 @@
    3.15    let
    3.16      fun mk_conj t u = @{term "op &"} $ t $ u
    3.17  
    3.18 -    fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
    3.19 +    fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
    3.20        | term_of (Assert ((n, t), v)) =
    3.21            mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
    3.22        | term_of (Ignore v) = term_of v
     4.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 26 13:44:50 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 26 20:51:17 2010 +0200
     4.3 @@ -3422,7 +3422,7 @@
     4.4  
     4.5  ML {*
     4.6    fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
     4.7 -    | calculated_subterms (@{const "op -->"} $ _ $ t) = calculated_subterms t
     4.8 +    | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
     4.9      | calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
    4.10      | calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
    4.11      | calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $ 
     5.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 26 13:44:50 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 26 20:51:17 2010 +0200
     5.3 @@ -1956,7 +1956,7 @@
     5.4        @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
     5.5    | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
     5.6        @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
     5.7 -  | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
     5.8 +  | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
     5.9        @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
    5.10    | fm_of_term ps vs (@{term "Not"} $ t') =
    5.11        @{code NOT} (fm_of_term ps vs t')
    5.12 @@ -2016,7 +2016,7 @@
    5.13  
    5.14  fun term_bools acc t =
    5.15    let
    5.16 -    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
    5.17 +    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
    5.18        @{term "op = :: int => _"}, @{term "op < :: int => _"},
    5.19        @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
    5.20        @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
     6.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 26 13:44:50 2010 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 26 20:51:17 2010 +0200
     6.3 @@ -1998,7 +1998,7 @@
     6.4        @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
     6.5    | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
     6.6    | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
     6.7 -  | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
     6.8 +  | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
     6.9    | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
    6.10    | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
    6.11        @{code E} (fm_of_term (("", dummyT) :: vs) p)
     7.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Aug 26 13:44:50 2010 +0200
     7.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Aug 26 20:51:17 2010 +0200
     7.3 @@ -5841,7 +5841,7 @@
     7.4        @{code And} (fm_of_term vs t1, fm_of_term vs t2)
     7.5    | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
     7.6        @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
     7.7 -  | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
     7.8 +  | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
     7.9        @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
    7.10    | fm_of_term vs (@{term "Not"} $ t') =
    7.11        @{code NOT} (fm_of_term vs t')
     8.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 26 13:44:50 2010 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 26 20:51:17 2010 +0200
     8.3 @@ -2956,7 +2956,7 @@
     8.4  val nott = @{term "Not"};
     8.5  val conjt = @{term "op &"};
     8.6  val disjt = @{term "op |"};
     8.7 -val impt = @{term "op -->"};
     8.8 +val impt = @{term HOL.implies};
     8.9  val ifft = @{term "op = :: bool => _"}
    8.10  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    8.11  fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    8.12 @@ -3020,7 +3020,7 @@
    8.13    | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
    8.14    | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
    8.15    | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
    8.16 -  | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    8.17 +  | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
    8.18    | Const(@{const_name "op ="},ty)$p$q => 
    8.19         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
    8.20         else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
     9.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 26 13:44:50 2010 +0200
     9.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 26 20:51:17 2010 +0200
     9.3 @@ -183,7 +183,7 @@
     9.4     | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
     9.5     | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
     9.6     | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
     9.7 -   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
     9.8 +   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
     9.9     | Const ("==>", _) $ _ $ _ => find_args bounds tm
    9.10     | Const ("==", _) $ _ $ _ => find_args bounds tm
    9.11     | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
    10.1 --- a/src/HOL/Decision_Procs/langford.ML	Thu Aug 26 13:44:50 2010 +0200
    10.2 +++ b/src/HOL/Decision_Procs/langford.ML	Thu Aug 26 20:51:17 2010 +0200
    10.3 @@ -185,7 +185,7 @@
    10.4     | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    10.5     | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    10.6     | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    10.7 -   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    10.8 +   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    10.9     | Const ("==>", _) $ _ $ _ => find_args bounds tm
   10.10     | Const ("==", _) $ _ $ _ => find_args bounds tm
   10.11     | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
    11.1 --- a/src/HOL/HOL.thy	Thu Aug 26 13:44:50 2010 +0200
    11.2 +++ b/src/HOL/HOL.thy	Thu Aug 26 20:51:17 2010 +0200
    11.3 @@ -56,13 +56,13 @@
    11.4    True          :: bool
    11.5    False         :: bool
    11.6    Not           :: "bool => bool"                   ("~ _" [40] 40)
    11.7 +  implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
    11.8  
    11.9  setup Sign.root_path
   11.10  
   11.11  consts
   11.12    "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
   11.13    "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
   11.14 -  "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
   11.15  
   11.16    "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
   11.17  
   11.18 @@ -91,7 +91,7 @@
   11.19    Not  ("\<not> _" [40] 40) and
   11.20    "op &"  (infixr "\<and>" 35) and
   11.21    "op |"  (infixr "\<or>" 30) and
   11.22 -  "op -->"  (infixr "\<longrightarrow>" 25) and
   11.23 +  HOL.implies  (infixr "\<longrightarrow>" 25) and
   11.24    not_equal  (infix "\<noteq>" 50)
   11.25  
   11.26  notation (HTML output)
   11.27 @@ -184,7 +184,7 @@
   11.28  
   11.29  finalconsts
   11.30    "op ="
   11.31 -  "op -->"
   11.32 +  HOL.implies
   11.33    The
   11.34  
   11.35  definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
    12.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 26 13:44:50 2010 +0200
    12.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 26 20:51:17 2010 +0200
    12.3 @@ -54,7 +54,7 @@
    12.4    ONE_ONE > HOL4Setup.ONE_ONE
    12.5    ONTO    > Fun.surj
    12.6    "=" > "op ="
    12.7 -  "==>" > "op -->"
    12.8 +  "==>" > HOL.implies
    12.9    "/\\" > "op &"
   12.10    "\\/" > "op |"
   12.11    "!" > All
    13.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 26 13:44:50 2010 +0200
    13.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 26 20:51:17 2010 +0200
    13.3 @@ -233,7 +233,7 @@
    13.4    "?" > "HOL.Ex"
    13.5    ">=" > "HOLLight.hollight.>="
    13.6    ">" > "HOLLight.hollight.>"
    13.7 -  "==>" > "op -->"
    13.8 +  "==>" > HOL.implies
    13.9    "=" > "op ="
   13.10    "<=" > "HOLLight.hollight.<="
   13.11    "<" > "HOLLight.hollight.<"
    14.1 --- a/src/HOL/Import/hol4rews.ML	Thu Aug 26 13:44:50 2010 +0200
    14.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Aug 26 20:51:17 2010 +0200
    14.3 @@ -628,7 +628,7 @@
    14.4              |> add_hol4_type_mapping "min" "fun" false "fun"
    14.5              |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
    14.6              |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
    14.7 -            |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
    14.8 +            |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
    14.9              |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
   14.10  in
   14.11  val hol4_setup =
    15.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Aug 26 13:44:50 2010 +0200
    15.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Aug 26 20:51:17 2010 +0200
    15.3 @@ -1205,7 +1205,7 @@
    15.4  fun non_trivial_term_consts t = fold_aterms
    15.5    (fn Const (c, _) =>
    15.6        if c = @{const_name Trueprop} orelse c = @{const_name All}
    15.7 -        orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
    15.8 +        orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
    15.9        then I else insert (op =) c
   15.10      | _ => I) t [];
   15.11  
   15.12 @@ -1214,7 +1214,7 @@
   15.13          fun add_consts (Const (c, _), cs) =
   15.14              (case c of
   15.15                   @{const_name "op ="} => insert (op =) "==" cs
   15.16 -               | @{const_name "op -->"} => insert (op =) "==>" cs
   15.17 +               | @{const_name HOL.implies} => insert (op =) "==>" cs
   15.18                 | @{const_name All} => cs
   15.19                 | "all" => cs
   15.20                 | @{const_name "op &"} => cs
   15.21 @@ -1860,7 +1860,7 @@
   15.22          val _ = if_debug pth hth
   15.23          val th1 = implies_elim_all (beta_eta_thm th)
   15.24          val a = case concl_of th1 of
   15.25 -                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
   15.26 +                    _ $ (Const(@{const_name HOL.implies},_) $ a $ Const(@{const_name False},_)) => a
   15.27                    | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
   15.28          val ca = cterm_of thy a
   15.29          val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
    16.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Aug 26 13:44:50 2010 +0200
    16.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Aug 26 20:51:17 2010 +0200
    16.3 @@ -1356,7 +1356,7 @@
    16.4  
    16.5  val known_sos_constants =
    16.6    [@{term "op ==>"}, @{term "Trueprop"},
    16.7 -   @{term "op -->"}, @{term "op &"}, @{term "op |"},
    16.8 +   @{term HOL.implies}, @{term "op &"}, @{term "op |"},
    16.9     @{term "Not"}, @{term "op = :: bool => _"},
   16.10     @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
   16.11     @{term "op = :: real => _"}, @{term "op < :: real => _"},
    17.1 --- a/src/HOL/Orderings.thy	Thu Aug 26 13:44:50 2010 +0200
    17.2 +++ b/src/HOL/Orderings.thy	Thu Aug 26 20:51:17 2010 +0200
    17.3 @@ -640,7 +640,7 @@
    17.4  let
    17.5    val All_binder = Syntax.binder_name @{const_syntax All};
    17.6    val Ex_binder = Syntax.binder_name @{const_syntax Ex};
    17.7 -  val impl = @{const_syntax "op -->"};
    17.8 +  val impl = @{const_syntax HOL.implies};
    17.9    val conj = @{const_syntax "op &"};
   17.10    val less = @{const_syntax less};
   17.11    val less_eq = @{const_syntax less_eq};
    18.1 --- a/src/HOL/Prolog/prolog.ML	Thu Aug 26 13:44:50 2010 +0200
    18.2 +++ b/src/HOL/Prolog/prolog.ML	Thu Aug 26 20:51:17 2010 +0200
    18.3 @@ -12,7 +12,7 @@
    18.4  fun isD t = case t of
    18.5      Const(@{const_name Trueprop},_)$t     => isD t
    18.6    | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
    18.7 -  | Const(@{const_name "op -->"},_)$l$r     => isG l andalso isD r
    18.8 +  | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
    18.9    | Const(   "==>",_)$l$r     => isG l andalso isD r
   18.10    | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   18.11    | Const("all",_)$Abs(s,_,t) => isD t
   18.12 @@ -32,7 +32,7 @@
   18.13      Const(@{const_name Trueprop},_)$t     => isG t
   18.14    | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
   18.15    | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
   18.16 -  | Const(@{const_name "op -->"},_)$l$r     => isD l andalso isG r
   18.17 +  | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
   18.18    | Const(   "==>",_)$l$r     => isD l andalso isG r
   18.19    | Const(@{const_name All},_)$Abs(_,_,t) => isG t
   18.20    | Const("all",_)$Abs(_,_,t) => isG t
   18.21 @@ -54,7 +54,7 @@
   18.22        _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
   18.23          (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
   18.24      | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   18.25 -    | _$(Const(@{const_name "op -->"},_)$_$_)     => at(thm RS mp)
   18.26 +    | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
   18.27      | _                             => [thm]
   18.28  in map zero_var_indexes (at thm) end;
   18.29  
   18.30 @@ -72,7 +72,7 @@
   18.31    -- is nice, but cannot instantiate unknowns in the assumptions *)
   18.32  fun hyp_resolve_tac i st = let
   18.33          fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
   18.34 -        |   ap (Const(@{const_name "op -->"},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   18.35 +        |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   18.36          |   ap t                          =                         (0,false,t);
   18.37  (*
   18.38          fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
    19.1 --- a/src/HOL/Set.thy	Thu Aug 26 13:44:50 2010 +0200
    19.2 +++ b/src/HOL/Set.thy	Thu Aug 26 20:51:17 2010 +0200
    19.3 @@ -219,7 +219,7 @@
    19.4    val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
    19.5    val All_binder = Syntax.binder_name @{const_syntax All};
    19.6    val Ex_binder = Syntax.binder_name @{const_syntax Ex};
    19.7 -  val impl = @{const_syntax "op -->"};
    19.8 +  val impl = @{const_syntax HOL.implies};
    19.9    val conj = @{const_syntax "op &"};
   19.10    val sbset = @{const_syntax subset};
   19.11    val sbset_eq = @{const_syntax subset_eq};
    20.1 --- a/src/HOL/TLA/Intensional.thy	Thu Aug 26 13:44:50 2010 +0200
    20.2 +++ b/src/HOL/TLA/Intensional.thy	Thu Aug 26 20:51:17 2010 +0200
    20.3 @@ -279,7 +279,7 @@
    20.4  
    20.5      fun hflatten t =
    20.6          case (concl_of t) of
    20.7 -          Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
    20.8 +          Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
    20.9          | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
   20.10    in
   20.11      hflatten t
    21.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Thu Aug 26 13:44:50 2010 +0200
    21.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Thu Aug 26 20:51:17 2010 +0200
    21.3 @@ -132,7 +132,7 @@
    21.4           Subset (to_R_rep Ts t1, to_R_rep Ts t2)
    21.5         | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
    21.6         | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
    21.7 -       | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
    21.8 +       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
    21.9         | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   21.10         | Free _ => raise SAME ()
   21.11         | Term.Var _ => raise SAME ()
   21.12 @@ -177,8 +177,8 @@
   21.13         | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
   21.14         | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   21.15         | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
   21.16 -       | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   21.17 -       | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
   21.18 +       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   21.19 +       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   21.20         | Const (@{const_name bot_class.bot},
   21.21                  T as Type (@{type_name fun}, [_, @{typ bool}])) =>
   21.22           empty_n_ary_rel (arity_of RRep card T)
    22.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 26 13:44:50 2010 +0200
    22.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 26 20:51:17 2010 +0200
    22.3 @@ -411,7 +411,7 @@
    22.4     (@{const_name "op ="}, 1),
    22.5     (@{const_name "op &"}, 2),
    22.6     (@{const_name "op |"}, 2),
    22.7 -   (@{const_name "op -->"}, 2),
    22.8 +   (@{const_name HOL.implies}, 2),
    22.9     (@{const_name If}, 3),
   22.10     (@{const_name Let}, 2),
   22.11     (@{const_name Pair}, 2),
   22.12 @@ -1454,7 +1454,7 @@
   22.13    | @{const Trueprop} $ t1 => lhs_of_equation t1
   22.14    | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   22.15    | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
   22.16 -  | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
   22.17 +  | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
   22.18    | _ => NONE
   22.19  fun is_constr_pattern _ (Bound _) = true
   22.20    | is_constr_pattern _ (Var _) = true
    23.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 26 13:44:50 2010 +0200
    23.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 26 20:51:17 2010 +0200
    23.3 @@ -774,7 +774,7 @@
    23.4                          (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
    23.5                        end))
    23.6           | (t0 as Const (@{const_name All}, _))
    23.7 -           $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
    23.8 +           $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
    23.9             do_bounded_quantifier t0 s' T' t10 t11 t12 accum
   23.10           | (t0 as Const (@{const_name Ex}, _))
   23.11             $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
   23.12 @@ -885,10 +885,10 @@
   23.13                  s0 = @{const_name Pure.conjunction} orelse
   23.14                  s0 = @{const_name "op &"} orelse
   23.15                  s0 = @{const_name "op |"} orelse
   23.16 -                s0 = @{const_name "op -->"} then
   23.17 +                s0 = @{const_name HOL.implies} then
   23.18                 let
   23.19                   val impl = (s0 = @{const_name "==>"} orelse
   23.20 -                             s0 = @{const_name "op -->"})
   23.21 +                             s0 = @{const_name HOL.implies})
   23.22                   val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
   23.23                   val (m2, accum) = do_formula sn t2 accum
   23.24                 in
   23.25 @@ -976,7 +976,7 @@
   23.26            | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
   23.27              consider_general_equals mdata true x t1 t2 accum
   23.28            | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
   23.29 -          | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   23.30 +          | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
   23.31            | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
   23.32                               \do_formula", [t])
   23.33      in do_formula t end
    24.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Aug 26 13:44:50 2010 +0200
    24.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Aug 26 20:51:17 2010 +0200
    24.3 @@ -522,7 +522,7 @@
    24.4            Op2 (And, bool_T, Any, sub' t1, sub' t2)
    24.5          | (Const (@{const_name "op |"}, _), [t1, t2]) =>
    24.6            Op2 (Or, bool_T, Any, sub t1, sub t2)
    24.7 -        | (Const (@{const_name "op -->"}, _), [t1, t2]) =>
    24.8 +        | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
    24.9            Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
   24.10          | (Const (@{const_name If}, T), [t1, t2, t3]) =>
   24.11            Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
    25.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 26 13:44:50 2010 +0200
    25.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 26 20:51:17 2010 +0200
    25.3 @@ -43,7 +43,7 @@
    25.4        | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
    25.5        | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
    25.6          aux def t1 andalso aux false t2
    25.7 -      | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2
    25.8 +      | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
    25.9        | aux def (t1 $ t2) = aux def t1 andalso aux def t2
   25.10        | aux def (t as Const (s, _)) =
   25.11          (not def orelse t <> @{const Suc}) andalso
   25.12 @@ -217,8 +217,8 @@
   25.13        | @{const "op |"} $ t1 $ t2 =>
   25.14          @{const "op |"} $ do_term new_Ts old_Ts polar t1
   25.15          $ do_term new_Ts old_Ts polar t2
   25.16 -      | @{const "op -->"} $ t1 $ t2 =>
   25.17 -        @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   25.18 +      | @{const HOL.implies} $ t1 $ t2 =>
   25.19 +        @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   25.20          $ do_term new_Ts old_Ts polar t2
   25.21        | Const (x as (s, T)) =>
   25.22          if is_descr s then
   25.23 @@ -334,7 +334,7 @@
   25.24          if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
   25.25        | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
   25.26          do_eq_or_imp Ts true def t0 t1 t2 seen
   25.27 -      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
   25.28 +      | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
   25.29          do_eq_or_imp Ts false def t0 t1 t2 seen
   25.30        | Abs (s, T, t') =>
   25.31          let val (t', seen) = do_term (T :: Ts) def t' [] seen in
   25.32 @@ -401,7 +401,7 @@
   25.33          t0 $ aux false t1 $ aux careful t2
   25.34        | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
   25.35          aux_eq careful true t0 t1 t2
   25.36 -      | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
   25.37 +      | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
   25.38          t0 $ aux false t1 $ aux careful t2
   25.39        | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
   25.40        | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
   25.41 @@ -608,8 +608,8 @@
   25.42            s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
   25.43          | @{const "op |"} $ t1 $ t2 =>
   25.44            s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
   25.45 -        | @{const "op -->"} $ t1 $ t2 =>
   25.46 -          @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   25.47 +        | @{const HOL.implies} $ t1 $ t2 =>
   25.48 +          @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   25.49            $ aux ss Ts js skolemizable polar t2
   25.50          | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
   25.51            t0 $ t1 $ aux ss Ts js skolemizable polar t2
   25.52 @@ -1121,7 +1121,7 @@
   25.53         (t10 as @{const "op |"}) $ t11 $ t12 =>
   25.54         t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
   25.55             $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
   25.56 -     | (t10 as @{const "op -->"}) $ t11 $ t12 =>
   25.57 +     | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
   25.58         t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
   25.59                                       $ Abs (s, T1, t11))
   25.60             $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
    26.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 13:44:50 2010 +0200
    26.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 20:51:17 2010 +0200
    26.3 @@ -595,10 +595,10 @@
    26.4  
    26.5  (* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
    26.6  
    26.7 -fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
    26.8 +fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
    26.9    | strip_imp_prems _ = [];
   26.10  
   26.11 -fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
   26.12 +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
   26.13    | strip_imp_concl A = A : term;
   26.14  
   26.15  fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    27.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 26 13:44:50 2010 +0200
    27.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 26 20:51:17 2010 +0200
    27.3 @@ -218,7 +218,7 @@
    27.4     @{const_name Trueprop},
    27.5     @{const_name Not},
    27.6     @{const_name "op ="},
    27.7 -   @{const_name "op -->"},
    27.8 +   @{const_name HOL.implies},
    27.9     @{const_name All},
   27.10     @{const_name Ex}, 
   27.11     @{const_name "op &"},
    28.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 13:44:50 2010 +0200
    28.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 20:51:17 2010 +0200
    28.3 @@ -168,10 +168,10 @@
    28.4      mk_split_lambda' xs t
    28.5    end;
    28.6  
    28.7 -fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
    28.8 +fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
    28.9    | strip_imp_prems _ = [];
   28.10  
   28.11 -fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
   28.12 +fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
   28.13    | strip_imp_concl A = A : term;
   28.14  
   28.15  fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    29.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 26 13:44:50 2010 +0200
    29.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 26 20:51:17 2010 +0200
    29.3 @@ -28,7 +28,7 @@
    29.4     @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    29.5     @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    29.6     @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
    29.7 -   @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
    29.8 +   @{term "op &"}, @{term "op |"}, @{term HOL.implies}, 
    29.9     @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
   29.10     @{term "op < :: int => _"}, @{term "op < :: nat => _"},
   29.11     @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
   29.12 @@ -569,7 +569,7 @@
   29.13  fun add_bools t =
   29.14    let
   29.15      val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
   29.16 -      @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
   29.17 +      @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
   29.18        @{term "Not"}, @{term "All :: (int => _) => _"},
   29.19        @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
   29.20      val is_op = member (op =) ops;
   29.21 @@ -616,7 +616,7 @@
   29.22        Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
   29.23    | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
   29.24        Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
   29.25 -  | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
   29.26 +  | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
   29.27        Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
   29.28    | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
   29.29        Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
   29.30 @@ -687,7 +687,7 @@
   29.31  
   29.32  fun strip_objimp ct =
   29.33    (case Thm.term_of ct of
   29.34 -    Const (@{const_name "op -->"}, _) $ _ $ _ =>
   29.35 +    Const (@{const_name HOL.implies}, _) $ _ $ _ =>
   29.36        let val (A, B) = Thm.dest_binop ct
   29.37        in A :: strip_objimp B end
   29.38    | _ => [ct]);
   29.39 @@ -712,7 +712,7 @@
   29.40       val qs = filter P ps
   29.41       val q = if P c then c else @{cterm "False"}
   29.42       val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
   29.43 -         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
   29.44 +         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
   29.45       val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
   29.46       val ntac = (case qs of [] => q aconvc @{cterm "False"}
   29.47                           | _ => false)
    30.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Thu Aug 26 13:44:50 2010 +0200
    30.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Aug 26 20:51:17 2010 +0200
    30.3 @@ -26,7 +26,7 @@
    30.4      Const(s,T)$_$_ => 
    30.5         if domain_type T = HOLogic.boolT
    30.6            andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
    30.7 -            @{const_name "op -->"}, @{const_name "op ="}] s
    30.8 +            @{const_name HOL.implies}, @{const_name "op ="}] s
    30.9         then binop_conv (conv env) p 
   30.10         else atcv env p
   30.11    | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
    31.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Aug 26 13:44:50 2010 +0200
    31.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Aug 26 20:51:17 2010 +0200
    31.3 @@ -161,7 +161,7 @@
    31.4    | conn @{const_name Not} = SOME "not"
    31.5    | conn @{const_name "op &"} = SOME "and"
    31.6    | conn @{const_name "op |"} = SOME "or"
    31.7 -  | conn @{const_name "op -->"} = SOME "implies"
    31.8 +  | conn @{const_name HOL.implies} = SOME "implies"
    31.9    | conn @{const_name "op ="} = SOME "iff"
   31.10    | conn @{const_name If} = SOME "if_then_else"
   31.11    | conn _ = NONE
    32.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Thu Aug 26 13:44:50 2010 +0200
    32.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Thu Aug 26 20:51:17 2010 +0200
    32.3 @@ -170,7 +170,7 @@
    32.4  val mk_true = @{cterm "~False"}
    32.5  val mk_false = @{cterm False}
    32.6  val mk_not = Thm.capply @{cterm Not}
    32.7 -val mk_implies = Thm.mk_binop @{cterm "op -->"}
    32.8 +val mk_implies = Thm.mk_binop @{cterm HOL.implies}
    32.9  val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
   32.10  
   32.11  fun mk_nary _ cu [] = cu
    33.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Thu Aug 26 13:44:50 2010 +0200
    33.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Thu Aug 26 20:51:17 2010 +0200
    33.3 @@ -198,7 +198,7 @@
    33.4        | @{term Not} $ _ => abstr1 cvs ct
    33.5        | @{term "op &"} $ _ $ _ => abstr2 cvs ct
    33.6        | @{term "op |"} $ _ $ _ => abstr2 cvs ct
    33.7 -      | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
    33.8 +      | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
    33.9        | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
   33.10        | Const (@{const_name distinct}, _) $ _ =>
   33.11            if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
    34.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Aug 26 13:44:50 2010 +0200
    34.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Aug 26 20:51:17 2010 +0200
    34.3 @@ -97,7 +97,7 @@
    34.4                 (@{const_name "op ="}, "equal"),
    34.5                 (@{const_name "op &"}, "and"),
    34.6                 (@{const_name "op |"}, "or"),
    34.7 -               (@{const_name "op -->"}, "implies"),
    34.8 +               (@{const_name HOL.implies}, "implies"),
    34.9                 (@{const_name Set.member}, "member"),
   34.10                 (@{const_name fequal}, "fequal"),
   34.11                 (@{const_name COMBI}, "COMBI"),
    35.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 13:44:50 2010 +0200
    35.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 20:51:17 2010 +0200
    35.3 @@ -161,7 +161,7 @@
    35.4          do_quantifier (pos = SOME true) body_t
    35.5        | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
    35.6        | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
    35.7 -      | @{const "op -->"} $ t1 $ t2 =>
    35.8 +      | @{const HOL.implies} $ t1 $ t2 =>
    35.9          do_formula (flip pos) t1 #> do_formula pos t2
   35.10        | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
   35.11          fold (do_term_or_formula T) [t1, t2]
   35.12 @@ -541,7 +541,7 @@
   35.13        | (_, @{const "==>"} $ t1 $ t2) =>
   35.14          do_formula (not pos) t1 andalso
   35.15          (t2 = @{prop False} orelse do_formula pos t2)
   35.16 -      | (_, @{const "op -->"} $ t1 $ t2) =>
   35.17 +      | (_, @{const HOL.implies} $ t1 $ t2) =>
   35.18          do_formula (not pos) t1 andalso
   35.19          (t2 = @{const False} orelse do_formula pos t2)
   35.20        | (_, @{const Not} $ t1) => do_formula (not pos) t1
    36.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 13:44:50 2010 +0200
    36.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 20:51:17 2010 +0200
    36.3 @@ -69,7 +69,7 @@
    36.4      Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
    36.5    | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    36.6      Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
    36.7 -  | negate_term (@{const "op -->"} $ t1 $ t2) =
    36.8 +  | negate_term (@{const HOL.implies} $ t1 $ t2) =
    36.9      @{const "op &"} $ t1 $ negate_term t2
   36.10    | negate_term (@{const "op &"} $ t1 $ t2) =
   36.11      @{const "op |"} $ negate_term t1 $ negate_term t2
    37.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 13:44:50 2010 +0200
    37.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 20:51:17 2010 +0200
    37.3 @@ -72,7 +72,7 @@
    37.4          do_quant bs AExists s T t'
    37.5        | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
    37.6        | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
    37.7 -      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
    37.8 +      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
    37.9        | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   37.10          do_conn bs AIff t1 t2
   37.11        | _ => (fn ts => do_term bs (Envir.eta_contract t)
   37.12 @@ -127,7 +127,7 @@
   37.13              aux Ts (t0 $ eta_expand Ts t1 1)
   37.14            | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   37.15            | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   37.16 -          | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   37.17 +          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   37.18            | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   37.19                $ t1 $ t2 =>
   37.20              t0 $ aux Ts t1 $ aux Ts t2
    38.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 26 13:44:50 2010 +0200
    38.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 26 20:51:17 2010 +0200
    38.3 @@ -128,7 +128,7 @@
    38.4  val dest_neg    = dest_monop @{const_name Not}
    38.5  val dest_pair   = dest_binop @{const_name Pair}
    38.6  val dest_eq     = dest_binop @{const_name "op ="}
    38.7 -val dest_imp    = dest_binop @{const_name "op -->"}
    38.8 +val dest_imp    = dest_binop @{const_name HOL.implies}
    38.9  val dest_conj   = dest_binop @{const_name "op &"}
   38.10  val dest_disj   = dest_binop @{const_name "op |"}
   38.11  val dest_select = dest_binder @{const_name Eps}
    39.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 26 13:44:50 2010 +0200
    39.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 26 20:51:17 2010 +0200
    39.3 @@ -159,7 +159,7 @@
    39.4  
    39.5  
    39.6  fun mk_imp{ant,conseq} =
    39.7 -   let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    39.8 +   let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    39.9     in list_comb(c,[ant,conseq])
   39.10     end;
   39.11  
   39.12 @@ -247,7 +247,7 @@
   39.13  fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
   39.14    | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
   39.15  
   39.16 -fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
   39.17 +fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
   39.18    | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
   39.19  
   39.20  fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
    40.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu Aug 26 13:44:50 2010 +0200
    40.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu Aug 26 20:51:17 2010 +0200
    40.3 @@ -97,7 +97,7 @@
    40.4    | is_atom (Const (@{const_name True}, _))                                            = false
    40.5    | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
    40.6    | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
    40.7 -  | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _)                                  = false
    40.8 +  | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
    40.9    | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   40.10    | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   40.11    | is_atom _                                                              = true;
   40.12 @@ -198,7 +198,7 @@
   40.13  	in
   40.14  		disj_cong OF [thm1, thm2]
   40.15  	end
   40.16 -  | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
   40.17 +  | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
   40.18  	let
   40.19  		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
   40.20  		val thm2 = make_nnf_thm thy y
   40.21 @@ -232,7 +232,7 @@
   40.22  	in
   40.23  		make_nnf_not_disj OF [thm1, thm2]
   40.24  	end
   40.25 -  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
   40.26 +  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
   40.27  	let
   40.28  		val thm1 = make_nnf_thm thy x
   40.29  		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
    41.1 --- a/src/HOL/Tools/groebner.ML	Thu Aug 26 13:44:50 2010 +0200
    41.2 +++ b/src/HOL/Tools/groebner.ML	Thu Aug 26 20:51:17 2010 +0200
    41.3 @@ -931,7 +931,7 @@
    41.4    | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
    41.5    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    41.6    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
    41.7 -  | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
    41.8 +  | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    41.9    | @{term "op ==>"} $_$_ => find_args bounds tm
   41.10    | Const("op ==",_)$_$_ => find_args bounds tm
   41.11    | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
    42.1 --- a/src/HOL/Tools/hologic.ML	Thu Aug 26 13:44:50 2010 +0200
    42.2 +++ b/src/HOL/Tools/hologic.ML	Thu Aug 26 20:51:17 2010 +0200
    42.3 @@ -210,8 +210,8 @@
    42.4  
    42.5  val conj = @{term "op &"}
    42.6  and disj = @{term "op |"}
    42.7 -and imp = @{term "op -->"}
    42.8 -and Not = @{term "Not"};
    42.9 +and imp = @{term implies}
   42.10 +and Not = @{term Not};
   42.11  
   42.12  fun mk_conj (t1, t2) = conj $ t1 $ t2
   42.13  and mk_disj (t1, t2) = disj $ t1 $ t2
   42.14 @@ -230,7 +230,7 @@
   42.15  
   42.16  fun disjuncts t = disjuncts_aux t [];
   42.17  
   42.18 -fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
   42.19 +fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
   42.20    | dest_imp  t = raise TERM ("dest_imp", [t]);
   42.21  
   42.22  fun dest_not (Const ("HOL.Not", _) $ t) = t
    43.1 --- a/src/HOL/Tools/meson.ML	Thu Aug 26 13:44:50 2010 +0200
    43.2 +++ b/src/HOL/Tools/meson.ML	Thu Aug 26 20:51:17 2010 +0200
    43.3 @@ -274,7 +274,7 @@
    43.4      | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
    43.5          if b then prod (signed_nclauses b t) (signed_nclauses b u)
    43.6               else sum (signed_nclauses b t) (signed_nclauses b u)
    43.7 -    | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
    43.8 +    | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
    43.9          if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
   43.10               else sum (signed_nclauses (not b) t) (signed_nclauses b u)
   43.11      | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
   43.12 @@ -401,7 +401,7 @@
   43.13    since this code expects to be called on a clause form.*)
   43.14  val is_conn = member (op =)
   43.15      [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
   43.16 -     @{const_name "op -->"}, @{const_name Not},
   43.17 +     @{const_name HOL.implies}, @{const_name Not},
   43.18       @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
   43.19  
   43.20  (*True if the term contains a function--not a logical connective--where the type
    44.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 26 13:44:50 2010 +0200
    44.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 26 20:51:17 2010 +0200
    44.3 @@ -342,7 +342,7 @@
    44.4      val bound_max = length Ts - 1;
    44.5      val bounds = map_index (fn (i, ty) =>
    44.6        (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
    44.7 -    fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
    44.8 +    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    44.9        | strip_imp A = ([], A)
   44.10      val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
   44.11      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
    45.1 --- a/src/HOL/Tools/refute.ML	Thu Aug 26 13:44:50 2010 +0200
    45.2 +++ b/src/HOL/Tools/refute.ML	Thu Aug 26 20:51:17 2010 +0200
    45.3 @@ -650,7 +650,7 @@
    45.4        | Const (@{const_name "op ="}, _) => t
    45.5        | Const (@{const_name "op &"}, _) => t
    45.6        | Const (@{const_name "op |"}, _) => t
    45.7 -      | Const (@{const_name "op -->"}, _) => t
    45.8 +      | Const (@{const_name HOL.implies}, _) => t
    45.9        (* sets *)
   45.10        | Const (@{const_name Collect}, _) => t
   45.11        | Const (@{const_name Set.member}, _) => t
   45.12 @@ -826,7 +826,7 @@
   45.13        | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
   45.14        | Const (@{const_name "op &"}, _) => axs
   45.15        | Const (@{const_name "op |"}, _) => axs
   45.16 -      | Const (@{const_name "op -->"}, _) => axs
   45.17 +      | Const (@{const_name HOL.implies}, _) => axs
   45.18        (* sets *)
   45.19        | Const (@{const_name Collect}, T) => collect_type_axioms T axs
   45.20        | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
   45.21 @@ -1895,7 +1895,7 @@
   45.22        (* this would make "undef" propagate, even for formulae like *)
   45.23        (* "True | undef":                                           *)
   45.24        (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
   45.25 -    | Const (@{const_name "op -->"}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
   45.26 +    | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
   45.27        (* 3-valued logic *)
   45.28        let
   45.29          val (i1, m1, a1) = interpret thy model args t1
   45.30 @@ -1905,9 +1905,9 @@
   45.31        in
   45.32          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   45.33        end
   45.34 -    | Const (@{const_name "op -->"}, _) $ t1 =>
   45.35 +    | Const (@{const_name HOL.implies}, _) $ t1 =>
   45.36        SOME (interpret thy model args (eta_expand t 1))
   45.37 -    | Const (@{const_name "op -->"}, _) =>
   45.38 +    | Const (@{const_name HOL.implies}, _) =>
   45.39        SOME (interpret thy model args (eta_expand t 2))
   45.40        (* this would make "undef" propagate, even for formulae like *)
   45.41        (* "False --> undef":                                        *)
    46.1 --- a/src/HOL/Tools/simpdata.ML	Thu Aug 26 13:44:50 2010 +0200
    46.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Aug 26 20:51:17 2010 +0200
    46.3 @@ -14,7 +14,7 @@
    46.4      | dest_eq _ = NONE;
    46.5    fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
    46.6      | dest_conj _ = NONE;
    46.7 -  fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
    46.8 +  fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
    46.9      | dest_imp _ = NONE;
   46.10    val conj = HOLogic.conj
   46.11    val imp  = HOLogic.imp
   46.12 @@ -159,7 +159,7 @@
   46.13    (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
   46.14  
   46.15  val mksimps_pairs =
   46.16 - [(@{const_name "op -->"}, [@{thm mp}]),
   46.17 + [(@{const_name HOL.implies}, [@{thm mp}]),
   46.18    (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
   46.19    (@{const_name All}, [@{thm spec}]),
   46.20    (@{const_name True}, []),
    47.1 --- a/src/HOL/ex/Meson_Test.thy	Thu Aug 26 13:44:50 2010 +0200
    47.2 +++ b/src/HOL/ex/Meson_Test.thy	Thu Aug 26 20:51:17 2010 +0200
    47.3 @@ -10,7 +10,7 @@
    47.4    below and constants declared in HOL!
    47.5  *}
    47.6  
    47.7 -hide_const (open) subset quotient union inter sum
    47.8 +hide_const (open) implies union inter subset sum quotient 
    47.9  
   47.10  text {*
   47.11    Test data for the MESON proof procedure
    48.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 26 13:44:50 2010 +0200
    48.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 26 20:51:17 2010 +0200
    48.3 @@ -90,7 +90,7 @@
    48.4      (*abstraction of a formula*)
    48.5      and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    48.6        | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    48.7 -      | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    48.8 +      | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    48.9        | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
   48.10        | fm ((c as Const(@{const_name True}, _))) = c
   48.11        | fm ((c as Const(@{const_name False}, _))) = c
    49.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Aug 26 13:44:50 2010 +0200
    49.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Aug 26 20:51:17 2010 +0200
    49.3 @@ -91,7 +91,7 @@
    49.4           in  case c of
    49.5               Const(@{const_name "op &"}, _)   => apply c (map tag ts)
    49.6             | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
    49.7 -           | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
    49.8 +           | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
    49.9             | Const(@{const_name Not}, _)    => apply c (map tag ts)
   49.10             | Const(@{const_name True}, _)   => (c, false)
   49.11             | Const(@{const_name False}, _)  => (c, false)
   49.12 @@ -187,7 +187,7 @@
   49.13              Buildin("AND", [fm pos p, fm pos q])
   49.14        | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
   49.15              Buildin("OR", [fm pos p, fm pos q])
   49.16 -      | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
   49.17 +      | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
   49.18              Buildin("=>", [fm (not pos) p, fm pos q])
   49.19        | fm pos (Const(@{const_name Not}, _) $ p) =
   49.20              Buildin("NOT", [fm (not pos) p])