equal
deleted
inserted
replaced
342 patterns (these are not perfect but work quite well): |
342 patterns (these are not perfect but work quite well): |
343 |
343 |
344 {)\([^\.]*\)\.\. -> {\1<\.\.} |
344 {)\([^\.]*\)\.\. -> {\1<\.\.} |
345 \.\.\([^(}]*\)(} -> \.\.<\1} |
345 \.\.\([^(}]*\)(} -> \.\.<\1} |
346 |
346 |
347 * theory Finite_Set: changed the syntax for 'setsum', summation over |
347 * Method comm_ring for proving equalities in commutative rings. |
|
348 |
|
349 * Theory Finite_Set: changed the syntax for 'setsum', summation over |
348 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is |
350 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is |
349 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can |
351 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can |
350 be a tuple pattern. |
352 be a tuple pattern. |
351 |
353 |
352 Some new syntax forms are available: |
354 Some new syntax forms are available: |