422 short_names is set, names are printed unqualified. If unique_names is |
422 short_names is set, names are printed unqualified. If unique_names is |
423 reset, the name prefix is reduced to the minimum required to achieve |
423 reset, the name prefix is reduced to the minimum required to achieve |
424 the original result when interning again, even if there is an overlap |
424 the original result when interning again, even if there is an overlap |
425 with earlier declarations. |
425 with earlier declarations. |
426 |
426 |
|
427 * Pure/sign/theory: discontinued named name spaces (i.e. classK, |
|
428 typeK, constK, axiomK, oracleK), but provide explicit operations for |
|
429 any of these kinds. For example, Sign.intern typeK is now |
|
430 Sign.intern_type, Theory.hide_space Sign.typeK is now |
|
431 Theory.hide_types. Also note that former |
|
432 Theory.hide_classes/types/consts are now |
|
433 Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions |
|
434 internalize their arguments! INCOMPATIBILITY. |
|
435 |
427 * Pure: cases produced by proof methods specify options, where NONE |
436 * Pure: cases produced by proof methods specify options, where NONE |
428 means to remove case bindings -- INCOMPATIBILITY in |
437 means to remove case bindings -- INCOMPATIBILITY in |
429 (RAW_)METHOD_CASES. |
438 (RAW_)METHOD_CASES. |
|
439 |
|
440 * Pure: the following operations retrieve axioms or theorems from a |
|
441 theory node or theory hierarchy, respectively: |
|
442 |
|
443 Theory.axioms_of: theory -> (string * term) list |
|
444 Theory.all_axioms_of: theory -> (string * term) list |
|
445 PureThy.thms_of: theory -> (string * thm) list |
|
446 PureThy.all_thms_of: theory -> (string * thm) list |
430 |
447 |
431 * Provers: Simplifier and Classical Reasoner now support proof context |
448 * Provers: Simplifier and Classical Reasoner now support proof context |
432 dependent plug-ins (simprocs, solvers, wrappers etc.). These extra |
449 dependent plug-ins (simprocs, solvers, wrappers etc.). These extra |
433 components are stored in the theory and patched into the |
450 components are stored in the theory and patched into the |
434 simpset/claset when used in an Isar proof context. Context dependent |
451 simpset/claset when used in an Isar proof context. Context dependent |