--- a/src/CCL/Wfd.thy Tue Sep 28 17:08:38 2021 +0200
+++ b/src/CCL/Wfd.thy Tue Sep 28 17:09:05 2021 +0200
@@ -441,7 +441,7 @@
fun is_rigid_prog t =
(case (Logic.strip_assums_concl t) of
- \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem _ for a _\<close>\<close>\<close> => null (Term.add_vars a [])
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem _ for a _\<close>\<close> => null (Term.add_vars a [])
| _ => false)
in
--- a/src/FOLP/IFOLP.thy Tue Sep 28 17:08:38 2021 +0200
+++ b/src/FOLP/IFOLP.thy Tue Sep 28 17:09:05 2021 +0200
@@ -612,7 +612,7 @@
structure Hypsubst = Hypsubst
(
(*Take apart an equality judgement; otherwise raise Match!*)
- fun dest_eq \<^Const_>\<open>Proof for \<open>\<^Const_>\<open>eq _ for t u\<close>\<close> _\<close> = (t, u);
+ fun dest_eq \<^Const_>\<open>Proof for \<^Const_>\<open>eq _ for t u\<close> _\<close> = (t, u);
val imp_intr = @{thm impI}
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML Tue Sep 28 17:09:05 2021 +0200
@@ -58,7 +58,7 @@
let
val T = Term.range_type (Term.fastype_of t)
val UNIV_const = \<^term>\<open>UNIV :: nat set\<close>
- in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end
+ in \<^Const>\<open>lub T for \<^Const>\<open>image \<^Type>\<open>nat\<close> T for t UNIV_const\<close>\<close> end
(*** Continuous function space ***)
--- a/src/HOL/Hoare/hoare_tac.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Tue Sep 28 17:09:05 2021 +0200
@@ -49,7 +49,7 @@
Abs (_, T, _) => T
| Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
in
- \<^Const>\<open>case_prod T T2 \<open>\<^Type>\<open>bool\<close>\<close> for \<open>absfree (x, T) z\<close>\<close>
+ \<^Const>\<open>case_prod T T2 \<^Type>\<open>bool\<close> for \<open>absfree (x, T) z\<close>\<close>
end;
(** maps [x1,...,xn] to (x1,...,xn) and types**)
--- a/src/HOL/Tools/Argo/argo_real.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML Tue Sep 28 17:09:05 2021 +0200
@@ -12,25 +12,25 @@
fun trans_type _ \<^Type>\<open>real\<close> tcx = SOME (Argo_Expr.Real, tcx)
| trans_type _ _ _ = NONE
-fun trans_term f \<^Const_>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+fun trans_term f \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t\<close> tcx =
tcx |> f t |>> Argo_Expr.mk_neg |> SOME
- | trans_term f \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME
- | trans_term f \<^Const_>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME
- | trans_term f \<^Const_>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME
- | trans_term f \<^Const_>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME
- | trans_term f \<^Const_>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>min \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME
- | trans_term f \<^Const_>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>max \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME
- | trans_term f \<^Const_>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+ | trans_term f \<^Const_>\<open>abs \<^Type>\<open>real\<close> for t\<close> tcx =
tcx |> f t |>> Argo_Expr.mk_abs |> SOME
- | trans_term f \<^Const_>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME
- | trans_term f \<^Const_>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME
| trans_term _ t tcx =
(case try HOLogic.dest_number t of
@@ -40,12 +40,12 @@
(* reverse translation *)
-fun mk_plus t1 t2 = \<^Const>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_plus t1 t2 = \<^Const>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close>
fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts)
-fun mk_times t1 t2 = \<^Const>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_divide t1 t2 = \<^Const>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_le t1 t2 = \<^Const>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_lt t1 t2 = \<^Const>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_times t1 t2 = \<^Const>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_divide t1 t2 = \<^Const>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_le t1 t2 = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_lt t1 t2 = \<^Const>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close>
fun mk_real_num i = HOLogic.mk_number \<^Type>\<open>real\<close> i
@@ -54,17 +54,17 @@
in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end
fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n)
- | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+ | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es))
| term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) =
- SOME \<^Const>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+ SOME \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) =
- SOME \<^Const>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+ SOME \<^Const>\<open>min \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) =
- SOME \<^Const>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
- | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+ SOME \<^Const>\<open>max \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+ | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2))
| term_of _ _ = NONE
@@ -97,10 +97,10 @@
local
-fun is_add2 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ _\<close> = true
+fun is_add2 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ _\<close> = true
| is_add2 _ = false
-fun is_add3 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ t\<close> = is_add2 t
+fun is_add3 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ t\<close> = is_add2 t
| is_add3 _ = false
val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp}
--- a/src/HOL/Tools/Argo/argo_tactic.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Tue Sep 28 17:09:05 2021 +0200
@@ -600,7 +600,7 @@
fun unclausify (thm, lits) ls =
(case (Thm.prop_of thm, lits) of
- (\<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>False\<close>\<close>\<close>, [(_, ct)]) =>
+ (\<^Const_>\<open>Trueprop for \<^Const_>\<open>False\<close>\<close>, [(_, ct)]) =>
let val thm = Thm.implies_intr ct thm
in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
| _ => (thm, Ord_List.union lit_ord lits ls))
--- a/src/HOL/Tools/Meson/meson.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Tue Sep 28 17:09:05 2021 +0200
@@ -261,9 +261,9 @@
fun refl_clause_aux 0 th = th
| refl_clause_aux n th =
case HOLogic.dest_Trueprop (Thm.concl_of th) of
- \<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close> =>
+ \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close> =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | \<^Const_>\<open>disj for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for t u\<close>\<close>\<close>\<close> _\<close> =>
+ | \<^Const_>\<open>disj for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t u\<close>\<close> _\<close> =>
if eliminable(t,u)
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*)
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*)
@@ -271,7 +271,7 @@
| _ => (*not a disjunction*) th;
fun notequal_lits_count \<^Const_>\<open>disj for P Q\<close> = notequal_lits_count P + notequal_lits_count Q
- | notequal_lits_count \<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for _ _\<close>\<close>\<close> = 1
+ | notequal_lits_count \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for _ _\<close>\<close> = 1
| notequal_lits_count _ = 0;
(*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -414,7 +414,7 @@
(**** Generation of contrapositives ****)
-fun is_left \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close>\<close>\<close> = true
+fun is_left \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close>\<close> = true
| is_left _ = false;
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -435,7 +435,7 @@
fun rigid t = not (is_Var (head_of t));
-fun ok4horn \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for t _\<close>\<close>\<close> = rigid t
+fun ok4horn \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for t _\<close>\<close> = rigid t
| ok4horn \<^Const_>\<open>Trueprop for t\<close> = rigid t
| ok4horn _ = false;
@@ -470,7 +470,7 @@
(***** MESON PROOF PROCEDURE *****)
-fun rhyps (\<^Const_>\<open>Pure.imp for \<open>\<^Const_>\<open>Trueprop for A\<close>\<close> phi\<close>, As) = rhyps(phi, A::As)
+fun rhyps (\<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for A\<close> phi\<close>, As) = rhyps(phi, A::As)
| rhyps (_, As) = As;
(** Detecting repeated assumptions in a subgoal **)
@@ -514,7 +514,7 @@
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
not_impD, not_iffD, not_allD, not_exD, not_notD];
-fun ok4nnf \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for t\<close>\<close>\<close> = rigid t
+fun ok4nnf \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for t\<close>\<close> = rigid t
| ok4nnf \<^Const_>\<open>Trueprop for t\<close> = rigid t
| ok4nnf _ = false;
@@ -620,7 +620,7 @@
(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
fun cong_extensionalize_thm ctxt th =
(case Thm.concl_of th of
- \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close>\<close>\<close> =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close> =>
(case get_F_pattern T t u of
SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
| NONE => th)
--- a/src/HOL/Transitive_Closure.thy Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Sep 28 17:09:05 2021 +0200
@@ -1289,7 +1289,7 @@
fun decomp \<^Const_>\<open>Trueprop for t\<close> =
let
- fun dec \<^Const_>\<open>Set.member _ for \<open>\<^Const_>\<open>Pair _ _ for a b\<close>\<close> rel\<close> =
+ fun dec \<^Const_>\<open>Set.member _ for \<^Const_>\<open>Pair _ _ for a b\<close> rel\<close> =
let
fun decr \<^Const_>\<open>rtrancl _ for r\<close> = (r,"r*")
| decr \<^Const_>\<open>trancl _ for r\<close> = (r,"r+")
--- a/src/HOL/Typerep.thy Tue Sep 28 17:08:38 2021 +0200
+++ b/src/HOL/Typerep.thy Tue Sep 28 17:09:05 2021 +0200
@@ -32,7 +32,7 @@
typed_print_translation \<open>
let
- fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<open>\<^Type>\<open>itself T\<close>\<close> _\<close>
+ fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<^Type>\<open>itself T\<close> _\<close>
(Const (\<^const_syntax>\<open>Pure.type\<close>, _) :: ts) =
Term.list_comb
(Syntax.const \<^syntax_const>\<open>_TYPEREP\<close> $ Syntax_Phases.term_of_typ ctxt T, ts)
--- a/src/ZF/Tools/inductive_package.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Sep 28 17:09:05 2021 +0200
@@ -298,7 +298,7 @@
(*Used to make induction rules;
ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
prem is a premise of an intr rule*)
- fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
+ fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close>, iprems) =
(case AList.lookup (op aconv) ind_alist X of
SOME pred => prem :: \<^make_judgment> (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
@@ -391,7 +391,7 @@
elem_factors ---> \<^Type>\<open>o\<close>)
val qconcl =
fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees
- \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for elem_tuple rec_tm\<close>\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
+ \<^Const>\<open>imp for \<^Const>\<open>mem for elem_tuple rec_tm\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
in (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
qconcl)
end;
@@ -400,7 +400,7 @@
(*Used to form simultaneous induction lemma*)
fun mk_rec_imp (rec_tm,pred) =
- \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close>\<close> \<open>pred $ Bound 0\<close>\<close>;
+ \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> \<open>pred $ Bound 0\<close>\<close>;
(*To instantiate the main induction rule*)
val induct_concl =
--- a/src/ZF/Tools/typechk.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/Tools/typechk.ML Tue Sep 28 17:09:05 2021 +0200
@@ -76,7 +76,7 @@
if length rls <= maxr then resolve_tac ctxt rls i else no_tac
end);
-fun is_rigid_elem \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for a _\<close>\<close>\<close> = not (is_Var (head_of a))
+fun is_rigid_elem \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for a _\<close>\<close> = not (is_Var (head_of a))
| is_rigid_elem _ = false;
(*Try solving a:A by assumption provided a is rigid!*)
--- a/src/ZF/arith_data.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/arith_data.ML Tue Sep 28 17:09:05 2021 +0200
@@ -48,7 +48,7 @@
(*Use <-> or = depending on the type of t*)
fun mk_eq_iff(t,u) =
if fastype_of t = \<^Type>\<open>i\<close>
- then \<^Const>\<open>IFOL.eq \<open>\<^Type>\<open>i\<close>\<close> for t u\<close>
+ then \<^Const>\<open>IFOL.eq \<^Type>\<open>i\<close> for t u\<close>
else \<^Const>\<open>IFOL.iff for t u\<close>;
(*We remove equality assumptions because they confuse the simplifier and
--- a/src/ZF/ind_syntax.ML Tue Sep 28 17:08:38 2021 +0200
+++ b/src/ZF/ind_syntax.ML Tue Sep 28 17:09:05 2021 +0200
@@ -22,7 +22,7 @@
fun mk_all_imp (A,P) =
let val T = \<^Type>\<open>i\<close> in
\<^Const>\<open>All T for
- \<open>Abs ("v", T, \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> A\<close>\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
+ \<open>Abs ("v", T, \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
end;
fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
@@ -37,7 +37,7 @@
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
- let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
+ let val \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close> = Logic.strip_imp_concl rl
in (t,X) end;
(*As above, but return error message if bad*)