1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML Thu Aug 26 20:14:39 2010 +0200
1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
2.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
3.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
4.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
5.2 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
6.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
7.2 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
8.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
9.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
10.2 +++ b/src/HOL/Decision_Procs/langford.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
11.2 +++ b/src/HOL/HOL.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
12.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
13.2 +++ b/src/HOL/Import/HOLLight/hollight.imp Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
14.2 +++ b/src/HOL/Import/hol4rews.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
15.2 +++ b/src/HOL/Import/proof_kernel.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
16.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
17.2 +++ b/src/HOL/Orderings.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
18.2 +++ b/src/HOL/Prolog/prolog.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
19.2 +++ b/src/HOL/Set.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
20.2 +++ b/src/HOL/TLA/Intensional.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
21.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
22.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
23.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
24.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
25.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
26.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
27.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
28.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
29.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
30.2 +++ b/src/HOL/Tools/Qelim/qelim.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
31.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
32.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
33.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
34.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
35.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
36.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
37.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
38.2 +++ b/src/HOL/Tools/TFL/dcterm.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
39.2 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
40.2 +++ b/src/HOL/Tools/cnf_funcs.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
41.2 +++ b/src/HOL/Tools/groebner.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
42.2 +++ b/src/HOL/Tools/hologic.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
43.2 +++ b/src/HOL/Tools/meson.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
44.2 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
45.2 +++ b/src/HOL/Tools/refute.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
46.2 +++ b/src/HOL/Tools/simpdata.ML Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
47.2 +++ b/src/HOL/ex/Meson_Test.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
48.2 +++ b/src/HOL/ex/SVC_Oracle.thy Thu Aug 26 20:51:29 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 20:14:39 2010 +0200
49.2 +++ b/src/HOL/ex/svc_funcs.ML Thu Aug 26 20:51:29 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])