equal
deleted
inserted
replaced
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 |
464 |
465 * Pure: 'class_deps' command visualizes the subclass relation, using |
465 * Pure: 'class_deps' command visualizes the subclass relation, using |
466 the graph browser tool. |
466 the graph browser tool. |
|
467 |
|
468 * Pure: 'print_theory' now suppresses entities with internal name |
|
469 (trailing "_") by default; use '!' option for full details. |
467 |
470 |
468 |
471 |
469 *** HOL *** |
472 *** HOL *** |
470 |
473 |
471 * New theory OperationalEquality providing class 'eq' with constant 'eq', |
474 * New theory OperationalEquality providing class 'eq' with constant 'eq', |