--- 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) ||
--- 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}) = []
--- 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
--- 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 $
--- 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"}]
--- 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)
--- 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')
--- 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))
--- 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)
--- 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)
--- 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
--- 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
--- 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.<"
--- 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 =
--- 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
--- 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 => _"},
--- 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};
--- 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
--- 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};
--- 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
--- 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)
--- 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
--- 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
--- 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)
--- 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))
--- 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);
--- 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 &"},
--- 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);
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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"),
--- 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
--- 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
--- 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
--- 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}
--- 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)
--- 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)
--- 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)
--- 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
--- 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
--- 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)
--- 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": *)
--- 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}, []),
--- 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
--- 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
--- 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])