580 PureThy.thms_of: theory -> (string * thm) list |
580 PureThy.thms_of: theory -> (string * thm) list |
581 PureThy.all_thms_of: theory -> (string * thm) list |
581 PureThy.all_thms_of: theory -> (string * thm) list |
582 |
582 |
583 * Pure: print_tac now outputs the goal through the trace channel. |
583 * Pure: print_tac now outputs the goal through the trace channel. |
584 |
584 |
585 * Provers: Simplifier and Classical Reasoner now support proof context |
585 * Pure/Simplifier: improved handling of bound variables (nameless |
586 dependent plug-ins (simprocs, solvers, wrappers etc.). These extra |
586 representation, avoid allocating new strings). Simprocs that invoke |
587 components are stored in the theory and patched into the |
587 the Simplifier recursively should use Simplifier.inherit_bounds to |
|
588 avoid local name clashes. |
|
589 |
|
590 * Pure/Provers: Simplifier and Classical Reasoner now support proof |
|
591 context dependent plug-ins (simprocs, solvers, wrappers etc.). These |
|
592 extra components are stored in the theory and patched into the |
588 simpset/claset when used in an Isar proof context. Context dependent |
593 simpset/claset when used in an Isar proof context. Context dependent |
589 components are maintained by the following theory operations: |
594 components are maintained by the following theory operations: |
590 |
595 |
591 Simplifier.add_context_simprocs |
596 Simplifier.add_context_simprocs |
592 Simplifier.del_context_simprocs |
597 Simplifier.del_context_simprocs |