equal
deleted
inserted
replaced
20 |
20 |
21 * Special treatment of ML file names has been discontinued. |
21 * Special treatment of ML file names has been discontinued. |
22 Historically, optional extensions .ML or .sml were added on demand -- |
22 Historically, optional extensions .ML or .sml were added on demand -- |
23 at the cost of clarity of file dependencies. Recall that Isabelle/ML |
23 at the cost of clarity of file dependencies. Recall that Isabelle/ML |
24 files exclusively use the .ML extension. Minor INCOMPATIBILTY. |
24 files exclusively use the .ML extension. Minor INCOMPATIBILTY. |
|
25 |
|
26 * Various options that affect document antiquotations are now properly |
|
27 handled within the context via configuration options, instead of |
|
28 unsynchronized references. There are both ML Config.T entities and |
|
29 Isar declaration attributes to access these. |
|
30 |
|
31 ML: Isar: |
|
32 |
|
33 Thy_Output.display thy_output_display |
|
34 Thy_Output.quotes thy_output_quotes |
|
35 Thy_Output.indent thy_output_indent |
|
36 Thy_Output.source thy_output_source |
|
37 Thy_Output.break thy_output_break |
|
38 |
|
39 Note that the corresponding "..._default" references may be only |
|
40 changed globally at the ROOT session setup, but *not* within a theory. |
25 |
41 |
26 |
42 |
27 *** Pure *** |
43 *** Pure *** |
28 |
44 |
29 * Interpretation command 'interpret' accepts a list of equations like |
45 * Interpretation command 'interpret' accepts a list of equations like |