equal
deleted
inserted
replaced
463 current background theory. Thus equivalent data produced in different |
463 current background theory. Thus equivalent data produced in different |
464 branches of the theory graph usually coincides (e.g. relevant for |
464 branches of the theory graph usually coincides (e.g. relevant for |
465 theory merge). Note that the softer Thm.eq_thm_prop is often more |
465 theory merge). Note that the softer Thm.eq_thm_prop is often more |
466 appropriate than Thm.eq_thm. |
466 appropriate than Thm.eq_thm. |
467 |
467 |
468 * Simplified programming interface to define ML antiquotations (to |
468 * Simplified programming interface to define ML antiquotations, see |
469 make it more close to the analogous Thy_Output.antiquotation). See |
469 structure ML_Antiquotation. Minor INCOMPATIBILITY. |
470 ML_Context.antiquotation and structure ML_Antiquotation. Minor |
|
471 INCOMPATIBILITY. |
|
472 |
470 |
473 * ML antiquotation @{here} refers to its source position, which is |
471 * ML antiquotation @{here} refers to its source position, which is |
474 occasionally useful for experimentation and diagnostic purposes. |
472 occasionally useful for experimentation and diagnostic purposes. |
475 |
473 |
476 * ML antiquotation @{path} produces a Path.T value, similarly to |
474 * ML antiquotation @{path} produces a Path.T value, similarly to |