equal
deleted
inserted
replaced
459 constant "_idtdummy" in the binding position. |
459 constant "_idtdummy" in the binding position. |
460 |
460 |
461 * Syntax: removed obsolete syntactic constant "_K" and its associated |
461 * Syntax: removed obsolete syntactic constant "_K" and its associated |
462 parse translation. INCOMPATIBILITY -- use dummy abstraction instead, |
462 parse translation. INCOMPATIBILITY -- use dummy abstraction instead, |
463 for example "A -> B" => "Pi A (%_. B)". |
463 for example "A -> B" => "Pi A (%_. B)". |
|
464 |
|
465 * Pure: 'class_deps' command visualizes the subclass relation, using |
|
466 the graph browser tool. |
464 |
467 |
465 |
468 |
466 *** HOL *** |
469 *** HOL *** |
467 |
470 |
468 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has been |
471 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has been |