equal
deleted
inserted
replaced
372 operations behave more similar to abbreviations. Potential |
372 operations behave more similar to abbreviations. Potential |
373 INCOMPATIBILITY in exotic situations. |
373 INCOMPATIBILITY in exotic situations. |
374 |
374 |
375 |
375 |
376 *** HOL *** |
376 *** HOL *** |
|
377 |
|
378 * Former "xsymbols" syntax with Isabelle symbols is used by default, |
|
379 without any special print mode. Important ASCII replacement syntax |
|
380 remains available under print mode "ASCII", but less important syntax |
|
381 has been removed (see below). |
377 |
382 |
378 * Combinator to represent case distinction on products is named "case_prod", |
383 * Combinator to represent case distinction on products is named "case_prod", |
379 uniformly, discontinuing any input aliasses. Very popular theorem aliasses |
384 uniformly, discontinuing any input aliasses. Very popular theorem aliasses |
380 have been retained. |
385 have been retained. |
381 Consolidated facts: |
386 Consolidated facts: |