equal
deleted
inserted
replaced
435 current background theory. Thus equivalent data produced in different |
435 current background theory. Thus equivalent data produced in different |
436 branches of the theory graph usually coincides (e.g. relevant for |
436 branches of the theory graph usually coincides (e.g. relevant for |
437 theory merge). Note that the softer Thm.eq_thm_prop is often more |
437 theory merge). Note that the softer Thm.eq_thm_prop is often more |
438 appropriate than Thm.eq_thm. |
438 appropriate than Thm.eq_thm. |
439 |
439 |
440 * Simplified programming interface to define ML antiquotations, see |
440 * Simplified programming interface to define ML antiquotations (to |
441 ML_Context.antiquotation, to make it more close to the analogous |
441 make it more close to the analogous Thy_Output.antiquotation). See |
442 Thy_Output.antiquotation. Minor INCOMPATIBILTY. |
442 ML_Context.antiquotation and structure ML_Antiquotation. Minor |
|
443 INCOMPATIBILITY. |
443 |
444 |
444 * ML antiquotation @{here} refers to its source position, which is |
445 * ML antiquotation @{here} refers to its source position, which is |
445 occasionally useful for experimentation and diagnostic purposes. |
446 occasionally useful for experimentation and diagnostic purposes. |
446 |
447 |
447 |
448 |