450 Theory.merge, etc.) |
450 Theory.merge, etc.) |
451 |
451 |
452 The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm |
452 The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm |
453 etc.) as well as the sign field in Thm.rep_thm etc. have been retained |
453 etc.) as well as the sign field in Thm.rep_thm etc. have been retained |
454 for convenience -- they merely return the theory. |
454 for convenience -- they merely return the theory. |
|
455 |
|
456 * Pure: the Isar proof context type is already defined early in Pure |
|
457 as Context.proof (note that ProofContext.context and Proof.context are |
|
458 aliases, where the latter is the preferred name). This enables other |
|
459 Isabelle components to refer to that type even before Isar is present. |
455 |
460 |
456 * Pure/sign/theory: discontinued named name spaces (i.e. classK, |
461 * Pure/sign/theory: discontinued named name spaces (i.e. classK, |
457 typeK, constK, axiomK, oracleK), but provide explicit operations for |
462 typeK, constK, axiomK, oracleK), but provide explicit operations for |
458 any of these kinds. For example, Sign.intern typeK is now |
463 any of these kinds. For example, Sign.intern typeK is now |
459 Sign.intern_type, Theory.hide_space Sign.typeK is now |
464 Sign.intern_type, Theory.hide_space Sign.typeK is now |