# HG changeset patch
# User haftmann
# Date 1282848677 -7200
# Node ID e46e7a9cb6226ea4f659bc5b7f7b7b6c00450ddf
# Parent  95df565aceb724605150e1a8b672cbed2e74469a
formerly unnamed infix impliciation now named HOL.implies

diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -504,7 +504,7 @@
         in
           Const (@{const_name If}, [@{typ bool}, T, T] ---> T) $ c $ t1 $ t2
         end) ||
-      binexp "implies" (binop @{term "op -->"}) ||
+      binexp "implies" (binop @{term HOL.implies}) ||
       scan_line "distinct" num :|-- scan_count exp >>
         (fn [] => @{term True}
           | ts as (t :: _) => mk_distinct (Term.fastype_of t) ts) ||
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Boogie/Tools/boogie_tactics.ML
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -53,7 +53,7 @@
   fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
     | explode_conj t = [t] 
 
-  fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
+  fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u)
     | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
     | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
     | splt (_, @{term True}) = []
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -59,8 +59,8 @@
     fun vc_of @{term True} = NONE
       | vc_of (@{term assert_at} $ Free (n, _) $ t) =
           SOME (Assert ((n, t), True))
-      | vc_of (@{term "op -->"} $ @{term True} $ u) = vc_of u
-      | vc_of (@{term "op -->"} $ t $ u) =
+      | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u
+      | vc_of (@{term HOL.implies} $ t $ u) =
           vc_of u |> Option.map (assume t)
       | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) =
           SOME (vc_of u |> the_default True |> assert (n, t))
@@ -76,7 +76,7 @@
   let
     fun mk_conj t u = @{term "op &"} $ t $ u
 
-    fun term_of (Assume (t, v)) = @{term "op -->"} $ t $ term_of v
+    fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v
       | term_of (Assert ((n, t), v)) =
           mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v)
       | term_of (Ignore v) = term_of v
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -3422,7 +3422,7 @@
 
 ML {*
   fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
-    | calculated_subterms (@{const "op -->"} $ _ $ t) = calculated_subterms t
+    | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
     | calculated_subterms (@{term "op <= :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
     | calculated_subterms (@{term "op < :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
     | calculated_subterms (@{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $ 
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -1956,7 +1956,7 @@
       @{code And} (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term "op |"} $ t1 $ t2) =
       @{code Or} (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (@{term "op -->"} $ t1 $ t2) =
+  | fm_of_term ps vs (@{term HOL.implies} $ t1 $ t2) =
       @{code Imp} (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term "Not"} $ t') =
       @{code NOT} (fm_of_term ps vs t')
@@ -2016,7 +2016,7 @@
 
 fun term_bools acc t =
   let
-    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+    val is_op = member (op =) [@{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
       @{term "op = :: int => _"}, @{term "op < :: int => _"},
       @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -1998,7 +1998,7 @@
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "op &"} $ t1 $ t2) = @{code And} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "op |"} $ t1 $ t2) = @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op -->"} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
+  | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) = @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "Not"} $ t') = @{code NOT} (fm_of_term vs t')
   | fm_of_term vs (Const (@{const_name Ex}, _) $ Abs (xn, xT, p)) =
       @{code E} (fm_of_term (("", dummyT) :: vs) p)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -5841,7 +5841,7 @@
       @{code And} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "op |"} $ t1 $ t2) =
       @{code Or} (fm_of_term vs t1, fm_of_term vs t2)
-  | fm_of_term vs (@{term "op -->"} $ t1 $ t2) =
+  | fm_of_term vs (@{term HOL.implies} $ t1 $ t2) =
       @{code Imp} (fm_of_term vs t1, fm_of_term vs t2)
   | fm_of_term vs (@{term "Not"} $ t') =
       @{code NOT} (fm_of_term vs t')
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -2956,7 +2956,7 @@
 val nott = @{term "Not"};
 val conjt = @{term "op &"};
 val disjt = @{term "op |"};
-val impt = @{term "op -->"};
+val impt = @{term HOL.implies};
 val ifft = @{term "op = :: bool => _"}
 fun llt rT = Const(@{const_name Orderings.less},rrT rT);
 fun lle rT = Const(@{const_name Orderings.less},rrT rT);
@@ -3020,7 +3020,7 @@
   | Const(@{const_name Not},_)$p => @{code NOT} (fm_of_term m m' p)
   | Const(@{const_name "op &"},_)$p$q => @{code And} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name "op |"},_)$p$q => @{code Or} (fm_of_term m m' p, fm_of_term m m' q)
-  | Const(@{const_name "op -->"},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
+  | Const(@{const_name HOL.implies},_)$p$q => @{code Imp} (fm_of_term m m' p, fm_of_term m m' q)
   | Const(@{const_name "op ="},ty)$p$q => 
        if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
        else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -183,7 +183,7 @@
    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
    | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -185,7 +185,7 @@
    | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
    | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
-   | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+   | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
    | Const ("==>", _) $ _ $ _ => find_args bounds tm
    | Const ("==", _) $ _ $ _ => find_args bounds tm
    | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -56,13 +56,13 @@
   True          :: bool
   False         :: bool
   Not           :: "bool => bool"                   ("~ _" [40] 40)
+  implies       :: "[bool, bool] => bool"           (infixr "-->" 25)
 
 setup Sign.root_path
 
 consts
   "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
   "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
-  "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
 
   "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
 
@@ -91,7 +91,7 @@
   Not  ("\<not> _" [40] 40) and
   "op &"  (infixr "\<and>" 35) and
   "op |"  (infixr "\<or>" 30) and
-  "op -->"  (infixr "\<longrightarrow>" 25) and
+  HOL.implies  (infixr "\<longrightarrow>" 25) and
   not_equal  (infix "\<noteq>" 50)
 
 notation (HTML output)
@@ -184,7 +184,7 @@
 
 finalconsts
   "op ="
-  "op -->"
+  HOL.implies
   The
 
 definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -54,7 +54,7 @@
   ONE_ONE > HOL4Setup.ONE_ONE
   ONTO    > Fun.surj
   "=" > "op ="
-  "==>" > "op -->"
+  "==>" > HOL.implies
   "/\\" > "op &"
   "\\/" > "op |"
   "!" > All
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 26 20:51:17 2010 +0200
@@ -233,7 +233,7 @@
   "?" > "HOL.Ex"
   ">=" > "HOLLight.hollight.>="
   ">" > "HOLLight.hollight.>"
-  "==>" > "op -->"
+  "==>" > HOL.implies
   "=" > "op ="
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -628,7 +628,7 @@
             |> add_hol4_type_mapping "min" "fun" false "fun"
             |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
             |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
-            |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
+            |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
             |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
 in
 val hol4_setup =
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -1205,7 +1205,7 @@
 fun non_trivial_term_consts t = fold_aterms
   (fn Const (c, _) =>
       if c = @{const_name Trueprop} orelse c = @{const_name All}
-        orelse c = @{const_name "op -->"} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
+        orelse c = @{const_name HOL.implies} orelse c = @{const_name "op &"} orelse c = @{const_name "op ="}
       then I else insert (op =) c
     | _ => I) t [];
 
@@ -1214,7 +1214,7 @@
         fun add_consts (Const (c, _), cs) =
             (case c of
                  @{const_name "op ="} => insert (op =) "==" cs
-               | @{const_name "op -->"} => insert (op =) "==>" cs
+               | @{const_name HOL.implies} => insert (op =) "==>" cs
                | @{const_name All} => cs
                | "all" => cs
                | @{const_name "op &"} => cs
@@ -1860,7 +1860,7 @@
         val _ = if_debug pth hth
         val th1 = implies_elim_all (beta_eta_thm th)
         val a = case concl_of th1 of
-                    _ $ (Const(@{const_name "op -->"},_) $ a $ Const(@{const_name False},_)) => a
+                    _ $ (Const(@{const_name HOL.implies},_) $ a $ Const(@{const_name False},_)) => a
                   | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
         val ca = cterm_of thy a
         val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -1356,7 +1356,7 @@
 
 val known_sos_constants =
   [@{term "op ==>"}, @{term "Trueprop"},
-   @{term "op -->"}, @{term "op &"}, @{term "op |"},
+   @{term HOL.implies}, @{term "op &"}, @{term "op |"},
    @{term "Not"}, @{term "op = :: bool => _"},
    @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
    @{term "op = :: real => _"}, @{term "op < :: real => _"},
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Orderings.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -640,7 +640,7 @@
 let
   val All_binder = Syntax.binder_name @{const_syntax All};
   val Ex_binder = Syntax.binder_name @{const_syntax Ex};
-  val impl = @{const_syntax "op -->"};
+  val impl = @{const_syntax HOL.implies};
   val conj = @{const_syntax "op &"};
   val less = @{const_syntax less};
   val less_eq = @{const_syntax less_eq};
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -12,7 +12,7 @@
 fun isD t = case t of
     Const(@{const_name Trueprop},_)$t     => isD t
   | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
-  | Const(@{const_name "op -->"},_)$l$r     => isG l andalso isD r
+  | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
   | Const(   "==>",_)$l$r     => isG l andalso isD r
   | Const(@{const_name All},_)$Abs(s,_,t) => isD t
   | Const("all",_)$Abs(s,_,t) => isD t
@@ -32,7 +32,7 @@
     Const(@{const_name Trueprop},_)$t     => isG t
   | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
   | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
-  | Const(@{const_name "op -->"},_)$l$r     => isD l andalso isG r
+  | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
   | Const(   "==>",_)$l$r     => isD l andalso isG r
   | Const(@{const_name All},_)$Abs(_,_,t) => isG t
   | Const("all",_)$Abs(_,_,t) => isG t
@@ -54,7 +54,7 @@
       _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
         (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
     | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
-    | _$(Const(@{const_name "op -->"},_)$_$_)     => at(thm RS mp)
+    | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
     | _                             => [thm]
 in map zero_var_indexes (at thm) end;
 
@@ -72,7 +72,7 @@
   -- is nice, but cannot instantiate unknowns in the assumptions *)
 fun hyp_resolve_tac i st = let
         fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
-        |   ap (Const(@{const_name "op -->"},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
+        |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
         |   ap t                          =                         (0,false,t);
 (*
         fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Set.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -219,7 +219,7 @@
   val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
   val All_binder = Syntax.binder_name @{const_syntax All};
   val Ex_binder = Syntax.binder_name @{const_syntax Ex};
-  val impl = @{const_syntax "op -->"};
+  val impl = @{const_syntax HOL.implies};
   val conj = @{const_syntax "op &"};
   val sbset = @{const_syntax subset};
   val sbset_eq = @{const_syntax subset_eq};
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/TLA/Intensional.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -279,7 +279,7 @@
 
     fun hflatten t =
         case (concl_of t) of
-          Const _ $ (Const (@{const_name "op -->"}, _) $ _ $ _) => hflatten (t RS mp)
+          Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
         | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
   in
     hflatten t
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -132,7 +132,7 @@
          Subset (to_R_rep Ts t1, to_R_rep Ts t2)
        | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
        | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
-       | @{const "op -->"} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
+       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
        | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
        | Free _ => raise SAME ()
        | Term.Var _ => raise SAME ()
@@ -177,8 +177,8 @@
        | @{const "op &"} => to_R_rep Ts (eta_expand Ts t 2)
        | @{const "op |"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
        | @{const "op |"} => to_R_rep Ts (eta_expand Ts t 2)
-       | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
-       | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
+       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
+       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name bot_class.bot},
                 T as Type (@{type_name fun}, [_, @{typ bool}])) =>
          empty_n_ary_rel (arity_of RRep card T)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -411,7 +411,7 @@
    (@{const_name "op ="}, 1),
    (@{const_name "op &"}, 2),
    (@{const_name "op |"}, 2),
-   (@{const_name "op -->"}, 2),
+   (@{const_name HOL.implies}, 2),
    (@{const_name If}, 3),
    (@{const_name Let}, 2),
    (@{const_name Pair}, 2),
@@ -1454,7 +1454,7 @@
   | @{const Trueprop} $ t1 => lhs_of_equation t1
   | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
   | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
-  | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
+  | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
   | _ => NONE
 fun is_constr_pattern _ (Bound _) = true
   | is_constr_pattern _ (Var _) = true
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -774,7 +774,7 @@
                         (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
                       end))
          | (t0 as Const (@{const_name All}, _))
-           $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
+           $ Abs (s', T', (t10 as @{const HOL.implies}) $ (t11 $ Bound 0) $ t12) =>
            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
          | (t0 as Const (@{const_name Ex}, _))
            $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
@@ -885,10 +885,10 @@
                 s0 = @{const_name Pure.conjunction} orelse
                 s0 = @{const_name "op &"} orelse
                 s0 = @{const_name "op |"} orelse
-                s0 = @{const_name "op -->"} then
+                s0 = @{const_name HOL.implies} then
                let
                  val impl = (s0 = @{const_name "==>"} orelse
-                             s0 = @{const_name "op -->"})
+                             s0 = @{const_name HOL.implies})
                  val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
                  val (m2, accum) = do_formula sn t2 accum
                in
@@ -976,7 +976,7 @@
           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
             consider_general_equals mdata true x t1 t2 accum
           | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
-          | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+          | (t0 as @{const HOL.implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
           | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
                              \do_formula", [t])
     in do_formula t end
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -522,7 +522,7 @@
           Op2 (And, bool_T, Any, sub' t1, sub' t2)
         | (Const (@{const_name "op |"}, _), [t1, t2]) =>
           Op2 (Or, bool_T, Any, sub t1, sub t2)
-        | (Const (@{const_name "op -->"}, _), [t1, t2]) =>
+        | (Const (@{const_name HOL.implies}, _), [t1, t2]) =>
           Op2 (Or, bool_T, Any, Op1 (Not, bool_T, Any, sub t1), sub' t2)
         | (Const (@{const_name If}, T), [t1, t2, t3]) =>
           Op3 (If, nth_range_type 3 T, Any, sub t1, sub t2, sub t3)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -43,7 +43,7 @@
       | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
       | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
         aux def t1 andalso aux false t2
-      | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2
+      | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
       | aux def (t1 $ t2) = aux def t1 andalso aux def t2
       | aux def (t as Const (s, _)) =
         (not def orelse t <> @{const Suc}) andalso
@@ -217,8 +217,8 @@
       | @{const "op |"} $ t1 $ t2 =>
         @{const "op |"} $ do_term new_Ts old_Ts polar t1
         $ do_term new_Ts old_Ts polar t2
-      | @{const "op -->"} $ t1 $ t2 =>
-        @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+      | @{const HOL.implies} $ t1 $ t2 =>
+        @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
         $ do_term new_Ts old_Ts polar t2
       | Const (x as (s, T)) =>
         if is_descr s then
@@ -334,7 +334,7 @@
         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
       | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
-      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+      | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
         do_eq_or_imp Ts false def t0 t1 t2 seen
       | Abs (s, T, t') =>
         let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -401,7 +401,7 @@
         t0 $ aux false t1 $ aux careful t2
       | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
         aux_eq careful true t0 t1 t2
-      | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
+      | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
         t0 $ aux false t1 $ aux careful t2
       | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
       | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
@@ -608,8 +608,8 @@
           s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
         | @{const "op |"} $ t1 $ t2 =>
           s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
-        | @{const "op -->"} $ t1 $ t2 =>
-          @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+        | @{const HOL.implies} $ t1 $ t2 =>
+          @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
           $ aux ss Ts js skolemizable polar t2
         | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
           t0 $ t1 $ aux ss Ts js skolemizable polar t2
@@ -1121,7 +1121,7 @@
        (t10 as @{const "op |"}) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
-     | (t10 as @{const "op -->"}) $ t11 $ t12 =>
+     | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
                                      $ Abs (s, T1, t11))
            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -595,10 +595,10 @@
 
 (* FIXME: large copy of Predicate_Compile_Quickcheck - refactor out commons *)
 
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = A : term;
 
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -218,7 +218,7 @@
    @{const_name Trueprop},
    @{const_name Not},
    @{const_name "op ="},
-   @{const_name "op -->"},
+   @{const_name HOL.implies},
    @{const_name All},
    @{const_name Ex}, 
    @{const_name "op &"},
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -168,10 +168,10 @@
     mk_split_lambda' xs t
   end;
 
-fun strip_imp_prems (Const(@{const_name "op -->"}, _) $ A $ B) = A :: strip_imp_prems B
+fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
   | strip_imp_prems _ = [];
 
-fun strip_imp_concl (Const(@{const_name "op -->"}, _) $ A $ B) = strip_imp_concl B
+fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B
   | strip_imp_concl A = A : term;
 
 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -28,7 +28,7 @@
    @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
-   @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
+   @{term "op &"}, @{term "op |"}, @{term HOL.implies}, 
    @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
@@ -569,7 +569,7 @@
 fun add_bools t =
   let
     val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
-      @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+      @{term "op &"}, @{term "op |"}, @{term HOL.implies}, @{term "op = :: bool => _"},
       @{term "Not"}, @{term "All :: (int => _) => _"},
       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
     val is_op = member (op =) ops;
@@ -616,7 +616,7 @@
       Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (Const (@{const_name "op |"}, _) $ t1 $ t2) =
       Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
-  | fm_of_term ps vs (Const (@{const_name "op -->"}, _) $ t1 $ t2) =
+  | fm_of_term ps vs (Const (@{const_name HOL.implies}, _) $ t1 $ t2) =
       Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
       Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
@@ -687,7 +687,7 @@
 
 fun strip_objimp ct =
   (case Thm.term_of ct of
-    Const (@{const_name "op -->"}, _) $ _ $ _ =>
+    Const (@{const_name HOL.implies}, _) $ _ $ _ =>
       let val (A, B) = Thm.dest_binop ct
       in A :: strip_objimp B end
   | _ => [ct]);
@@ -712,7 +712,7 @@
      val qs = filter P ps
      val q = if P c then c else @{cterm "False"}
      val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
-         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
+         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
      val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
      val ntac = (case qs of [] => q aconvc @{cterm "False"}
                          | _ => false)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -26,7 +26,7 @@
     Const(s,T)$_$_ => 
        if domain_type T = HOLogic.boolT
           andalso member (op =) [@{const_name "op &"}, @{const_name "op |"},
-            @{const_name "op -->"}, @{const_name "op ="}] s
+            @{const_name HOL.implies}, @{const_name "op ="}] s
        then binop_conv (conv env) p 
        else atcv env p
   | Const(@{const_name Not},_)$_ => arg_conv (conv env) p
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -161,7 +161,7 @@
   | conn @{const_name Not} = SOME "not"
   | conn @{const_name "op &"} = SOME "and"
   | conn @{const_name "op |"} = SOME "or"
-  | conn @{const_name "op -->"} = SOME "implies"
+  | conn @{const_name HOL.implies} = SOME "implies"
   | conn @{const_name "op ="} = SOME "iff"
   | conn @{const_name If} = SOME "if_then_else"
   | conn _ = NONE
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -170,7 +170,7 @@
 val mk_true = @{cterm "~False"}
 val mk_false = @{cterm False}
 val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm "op -->"}
+val mk_implies = Thm.mk_binop @{cterm HOL.implies}
 val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
 
 fun mk_nary _ cu [] = cu
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -198,7 +198,7 @@
       | @{term Not} $ _ => abstr1 cvs ct
       | @{term "op &"} $ _ $ _ => abstr2 cvs ct
       | @{term "op |"} $ _ $ _ => abstr2 cvs ct
-      | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
+      | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name distinct}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -97,7 +97,7 @@
                (@{const_name "op ="}, "equal"),
                (@{const_name "op &"}, "and"),
                (@{const_name "op |"}, "or"),
-               (@{const_name "op -->"}, "implies"),
+               (@{const_name HOL.implies}, "implies"),
                (@{const_name Set.member}, "member"),
                (@{const_name fequal}, "fequal"),
                (@{const_name COMBI}, "COMBI"),
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -161,7 +161,7 @@
         do_quantifier (pos = SOME true) body_t
       | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
       | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
-      | @{const "op -->"} $ t1 $ t2 =>
+      | @{const HOL.implies} $ t1 $ t2 =>
         do_formula (flip pos) t1 #> do_formula pos t2
       | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
         fold (do_term_or_formula T) [t1, t2]
@@ -541,7 +541,7 @@
       | (_, @{const "==>"} $ t1 $ t2) =>
         do_formula (not pos) t1 andalso
         (t2 = @{prop False} orelse do_formula pos t2)
-      | (_, @{const "op -->"} $ t1 $ t2) =>
+      | (_, @{const HOL.implies} $ t1 $ t2) =>
         do_formula (not pos) t1 andalso
         (t2 = @{const False} orelse do_formula pos t2)
       | (_, @{const Not} $ t1) => do_formula (not pos) t1
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -69,7 +69,7 @@
     Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
     Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
-  | negate_term (@{const "op -->"} $ t1 $ t2) =
+  | negate_term (@{const HOL.implies} $ t1 $ t2) =
     @{const "op &"} $ t1 $ negate_term t2
   | negate_term (@{const "op &"} $ t1 $ t2) =
     @{const "op |"} $ negate_term t1 $ negate_term t2
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -72,7 +72,7 @@
         do_quant bs AExists s T t'
       | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
       | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
-      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+      | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
       | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
         do_conn bs AIff t1 t2
       | _ => (fn ts => do_term bs (Envir.eta_contract t)
@@ -127,7 +127,7 @@
             aux Ts (t0 $ eta_expand Ts t1 1)
           | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
-          | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
               $ t1 $ t2 =>
             t0 $ aux Ts t1 $ aux Ts t2
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/TFL/dcterm.ML
--- a/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -128,7 +128,7 @@
 val dest_neg    = dest_monop @{const_name Not}
 val dest_pair   = dest_binop @{const_name Pair}
 val dest_eq     = dest_binop @{const_name "op ="}
-val dest_imp    = dest_binop @{const_name "op -->"}
+val dest_imp    = dest_binop @{const_name HOL.implies}
 val dest_conj   = dest_binop @{const_name "op &"}
 val dest_disj   = dest_binop @{const_name "op |"}
 val dest_select = dest_binder @{const_name Eps}
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -159,7 +159,7 @@
 
 
 fun mk_imp{ant,conseq} =
-   let val c = Const(@{const_name "op -->"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[ant,conseq])
    end;
 
@@ -247,7 +247,7 @@
 fun dest_eq(Const(@{const_name "op ="},_) $ M $ N) = {lhs=M, rhs=N}
   | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
 
-fun dest_imp(Const(@{const_name "op -->"},_) $ M $ N) = {ant=M, conseq=N}
+fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
   | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
 
 fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -97,7 +97,7 @@
   | is_atom (Const (@{const_name True}, _))                                            = false
   | is_atom (Const (@{const_name "op &"}, _) $ _ $ _)                                    = false
   | is_atom (Const (@{const_name "op |"}, _) $ _ $ _)                                    = false
-  | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _)                                  = false
+  | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _)                                  = false
   | is_atom (Const (@{const_name "op ="}, Type ("fun", @{typ bool} :: _)) $ _ $ _)       = false
   | is_atom (Const (@{const_name Not}, _) $ _)                                         = false
   | is_atom _                                                              = true;
@@ -198,7 +198,7 @@
 	in
 		disj_cong OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
+  | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
 	let
 		val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
 		val thm2 = make_nnf_thm thy y
@@ -232,7 +232,7 @@
 	in
 		make_nnf_not_disj OF [thm1, thm2]
 	end
-  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
+  | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
 	let
 		val thm1 = make_nnf_thm thy x
 		val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -931,7 +931,7 @@
   | Const (@{const_name Ex}, _) $ _ => find_body bounds (dest_arg tm)
   | Const (@{const_name "op &"}, _) $ _ $ _ => find_args bounds tm
   | Const (@{const_name "op |"}, _) $ _ $ _ => find_args bounds tm
-  | Const (@{const_name "op -->"}, _) $ _ $ _ => find_args bounds tm
+  | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
   | @{term "op ==>"} $_$_ => find_args bounds tm
   | Const("op ==",_)$_$_ => find_args bounds tm
   | @{term Trueprop}$_ => find_term bounds (dest_arg tm)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -210,8 +210,8 @@
 
 val conj = @{term "op &"}
 and disj = @{term "op |"}
-and imp = @{term "op -->"}
-and Not = @{term "Not"};
+and imp = @{term implies}
+and Not = @{term Not};
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2
@@ -230,7 +230,7 @@
 
 fun disjuncts t = disjuncts_aux t [];
 
-fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
+fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
 fun dest_not (Const ("HOL.Not", _) $ t) = t
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -274,7 +274,7 @@
     | signed_nclauses b (Const(@{const_name "op |"},_) $ t $ u) =
         if b then prod (signed_nclauses b t) (signed_nclauses b u)
              else sum (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(@{const_name "op -->"},_) $ t $ u) =
+    | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) =
         if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
              else sum (signed_nclauses (not b) t) (signed_nclauses b u)
     | signed_nclauses b (Const(@{const_name "op ="}, Type ("fun", [T, _])) $ t $ u) =
@@ -401,7 +401,7 @@
   since this code expects to be called on a clause form.*)
 val is_conn = member (op =)
     [@{const_name Trueprop}, @{const_name "op &"}, @{const_name "op |"},
-     @{const_name "op -->"}, @{const_name Not},
+     @{const_name HOL.implies}, @{const_name Not},
      @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}];
 
 (*True if the term contains a function--not a logical connective--where the type
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -342,7 +342,7 @@
     val bound_max = length Ts - 1;
     val bounds = map_index (fn (i, ty) =>
       (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
-    fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B)
+    fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
       | strip_imp A = ([], A)
     val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds);
     val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -650,7 +650,7 @@
       | Const (@{const_name "op ="}, _) => t
       | Const (@{const_name "op &"}, _) => t
       | Const (@{const_name "op |"}, _) => t
-      | Const (@{const_name "op -->"}, _) => t
+      | Const (@{const_name HOL.implies}, _) => t
       (* sets *)
       | Const (@{const_name Collect}, _) => t
       | Const (@{const_name Set.member}, _) => t
@@ -826,7 +826,7 @@
       | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
       | Const (@{const_name "op &"}, _) => axs
       | Const (@{const_name "op |"}, _) => axs
-      | Const (@{const_name "op -->"}, _) => axs
+      | Const (@{const_name HOL.implies}, _) => axs
       (* sets *)
       | Const (@{const_name Collect}, T) => collect_type_axioms T axs
       | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
@@ -1895,7 +1895,7 @@
       (* this would make "undef" propagate, even for formulae like *)
       (* "True | undef":                                           *)
       (* SOME (Node [Node [TT, TT], Node [TT, FF]], model, args) *)
-    | Const (@{const_name "op -->"}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
+    | Const (@{const_name HOL.implies}, _) $ t1 $ t2 =>  (* similar to "==>" (Pure) *)
       (* 3-valued logic *)
       let
         val (i1, m1, a1) = interpret thy model args t1
@@ -1905,9 +1905,9 @@
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-    | Const (@{const_name "op -->"}, _) $ t1 =>
+    | Const (@{const_name HOL.implies}, _) $ t1 =>
       SOME (interpret thy model args (eta_expand t 1))
-    | Const (@{const_name "op -->"}, _) =>
+    | Const (@{const_name HOL.implies}, _) =>
       SOME (interpret thy model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "False --> undef":                                        *)
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/Tools/simpdata.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -14,7 +14,7 @@
     | dest_eq _ = NONE;
   fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
     | dest_conj _ = NONE;
-  fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
+  fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
     | dest_imp _ = NONE;
   val conj = HOLogic.conj
   val imp  = HOLogic.imp
@@ -159,7 +159,7 @@
   (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
 
 val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
+ [(@{const_name HOL.implies}, [@{thm mp}]),
   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
   (@{const_name All}, [@{thm spec}]),
   (@{const_name True}, []),
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -10,7 +10,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) subset quotient union inter sum
+hide_const (open) implies union inter subset sum quotient 
 
 text {*
   Test data for the MESON proof procedure
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -90,7 +90,7 @@
     (*abstraction of a formula*)
     and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
-      | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+      | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
       | fm ((c as Const(@{const_name True}, _))) = c
       | fm ((c as Const(@{const_name False}, _))) = c
diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Thu Aug 26 20:51:17 2010 +0200
@@ -91,7 +91,7 @@
          in  case c of
              Const(@{const_name "op &"}, _)   => apply c (map tag ts)
            | Const(@{const_name "op |"}, _)   => apply c (map tag ts)
-           | Const(@{const_name "op -->"}, _) => apply c (map tag ts)
+           | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
            | Const(@{const_name Not}, _)    => apply c (map tag ts)
            | Const(@{const_name True}, _)   => (c, false)
            | Const(@{const_name False}, _)  => (c, false)
@@ -187,7 +187,7 @@
             Buildin("AND", [fm pos p, fm pos q])
       | fm pos (Const(@{const_name "op |"}, _) $ p $ q) =
             Buildin("OR", [fm pos p, fm pos q])
-      | fm pos (Const(@{const_name "op -->"}, _) $ p $ q) =
+      | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
             Buildin("=>", [fm (not pos) p, fm pos q])
       | fm pos (Const(@{const_name Not}, _) $ p) =
             Buildin("NOT", [fm (not pos) p])