equal
deleted
inserted
replaced
339 optional ('?'). The old synatx '!' has been discontinued. |
339 optional ('?'). The old synatx '!' has been discontinued. |
340 INCOMPATIBILITY, remove '!' and add '?' as required. |
340 INCOMPATIBILITY, remove '!' and add '?' as required. |
341 |
341 |
342 * Keyword 'rewrites' identifies rewrite morphisms in interpretation |
342 * Keyword 'rewrites' identifies rewrite morphisms in interpretation |
343 commands. Previously, the keyword was 'where'. INCOMPATIBILITY. |
343 commands. Previously, the keyword was 'where'. INCOMPATIBILITY. |
|
344 |
|
345 * Special notation \<struct> for the first implicit 'structure' in the context |
|
346 has been discontinued. Rare INCOMPATIBILITY, use explicit structure name |
|
347 instead, notably in indexed notation with block-subscript (e.g. \<odot>\<^bsub>A\<^esub>). |
344 |
348 |
345 * More gentle suppression of syntax along locale morphisms while |
349 * More gentle suppression of syntax along locale morphisms while |
346 printing terms. Previously 'abbreviation' and 'notation' declarations |
350 printing terms. Previously 'abbreviation' and 'notation' declarations |
347 would be suppressed for morphisms except term identity. Now |
351 would be suppressed for morphisms except term identity. Now |
348 'abbreviation' is also kept for morphims that only change the involved |
352 'abbreviation' is also kept for morphims that only change the involved |