equal
deleted
inserted
replaced
511 |
511 |
512 * Unions and Intersections over Intervals: |
512 * Unions and Intersections over Intervals: |
513 There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is |
513 There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is |
514 also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" |
514 also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A" |
515 like in normal math, and corresponding versions for < and for intersection. |
515 like in normal math, and corresponding versions for < and for intersection. |
|
516 |
|
517 * HOL/List: Ordering "lexico" is renamed "lenlex" and the standard |
|
518 lexicographic dictonary ordering has been added as "lexord". |
516 |
519 |
517 * ML: the legacy theory structures Int and List have been removed. They had |
520 * ML: the legacy theory structures Int and List have been removed. They had |
518 conflicted with ML Basis Library structures having the same names. |
521 conflicted with ML Basis Library structures having the same names. |
519 |
522 |
520 * 'refute' command added to search for (finite) countermodels. Only works |
523 * 'refute' command added to search for (finite) countermodels. Only works |