equal
deleted
inserted
replaced
601 higher-order interface for components with shared state, avoiding the |
601 higher-order interface for components with shared state, avoiding the |
602 delicate details of mutexes and condition variables. [Poly/ML 5.2.1 |
602 delicate details of mutexes and condition variables. [Poly/ML 5.2.1 |
603 or later] |
603 or later] |
604 |
604 |
605 * Simplified ML attribute and method setup, cf. functions Attrib.setup |
605 * Simplified ML attribute and method setup, cf. functions Attrib.setup |
606 and Method.setup, as well as commands 'attribute_setup'. |
606 and Method.setup, as well as commands 'attribute_setup' and |
|
607 'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify |
|
608 existing code accordingly, or use plain 'setup' together with old |
|
609 Method.add_method. |
607 |
610 |
608 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
611 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
609 to 'a -> thm, while results are always tagged with an authentic oracle |
612 to 'a -> thm, while results are always tagged with an authentic oracle |
610 name. The Isar command 'oracle' is now polymorphic, no argument type |
613 name. The Isar command 'oracle' is now polymorphic, no argument type |
611 is specified. INCOMPATIBILITY, need to simplify existing oracle code |
614 is specified. INCOMPATIBILITY, need to simplify existing oracle code |