# HG changeset patch # User wenzelm # Date 1724593983 -7200 # Node ID 1d8ce19d7d71789a6c335e52fcc3fc6dd4edb3bb # Parent 47c0aa388621d34f3599b3f07f70155c193080b2 proper translation for "_qprod", following "_qsum" (see also e14b89d6ef13 and fa7d27ef7e59); diff -r 47c0aa388621 -r 1d8ce19d7d71 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Sun Aug 25 15:40:07 2024 +0200 +++ b/src/HOL/Groups_Big.thy Sun Aug 25 15:53:03 2024 +0200 @@ -1445,6 +1445,22 @@ translations "\x|P. t" => "CONST prod (\x. t) {x. P}" +print_translation \ + let + fun prod_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = + if x <> y then raise Match + else + let + val x' = Syntax_Trans.mark_bound_body (x, Tx); + val t' = subst_bound (x', t); + val P' = subst_bound (x', P); + in + Syntax.const \<^syntax_const>\_qprod\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' + end + | prod_tr' _ = raise Match; + in [(\<^const_syntax>\prod\, K prod_tr')] end +\ + context comm_monoid_mult begin