equal
deleted
inserted
replaced
531 d) ML code directly refering to constant names |
531 d) ML code directly refering to constant names |
532 This in general only affects hand-written proof tactics, simprocs and so on. |
532 This in general only affects hand-written proof tactics, simprocs and so on. |
533 INCOMPATIBILITY: grep your sourcecode and replace names. |
533 INCOMPATIBILITY: grep your sourcecode and replace names. |
534 |
534 |
535 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). |
535 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). |
|
536 |
|
537 * Relation composition operator "op O" now has precedence 75 and binds |
|
538 stronger than union and intersection. INCOMPATIBILITY. |
536 |
539 |
537 * The old set interval syntax "{m..n(}" (and relatives) has been removed. |
540 * The old set interval syntax "{m..n(}" (and relatives) has been removed. |
538 Use "{m..<n}" (and relatives) instead. |
541 Use "{m..<n}" (and relatives) instead. |
539 |
542 |
540 * In the context of the assumption "~(s = t)" the Simplifier rewrites |
543 * In the context of the assumption "~(s = t)" the Simplifier rewrites |