equal
deleted
inserted
replaced
9 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
9 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
10 p $ u $ rev_sum t |
10 p $ u $ rev_sum t |
11 | rev_sum t = t *} |
11 | rev_sum t = t *} |
12 |
12 |
13 text {* |
13 text {* |
14 An alternative solution using the function @{ML [index] mk_binop in HOLogic} is: |
14 An alternative solution using the function @{ML_ind mk_binop in HOLogic} is: |
15 *} |
15 *} |
16 |
16 |
17 ML{*fun rev_sum t = |
17 ML{*fun rev_sum t = |
18 let |
18 let |
19 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
19 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |