equal
deleted
inserted
replaced
84 let |
84 let |
85 fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = |
85 fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = |
86 if x <> y then raise Match |
86 if x <> y then raise Match |
87 else |
87 else |
88 let |
88 let |
89 val x' = Syntax.mark_bound x; |
89 val x' = Syntax_Trans.mark_bound x; |
90 val t' = subst_bound (x', t); |
90 val t' = subst_bound (x', t); |
91 val P' = subst_bound (x', P); |
91 val P' = subst_bound (x', P); |
92 in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end |
92 in Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound x $ P' $ t' end |
93 | setsum_tr' _ = raise Match; |
93 | setsum_tr' _ = raise Match; |
94 in [(@{const_syntax setsum}, setsum_tr')] end |
94 in [(@{const_syntax setsum}, setsum_tr')] end |
95 *} |
95 *} |
96 |
96 |
97 lemma setsum_empty: |
97 lemma setsum_empty: |