NEWS
changeset 20620 8b26f58c5646
parent 20607 926a76a84e97
child 20712 b3cd1233167f
equal deleted inserted replaced
20619:02e9b54b18fd 20620:8b26f58c5646
   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',