equal
deleted
inserted
replaced
46 etc.) may depend on the signature of the theory context being |
46 etc.) may depend on the signature of the theory context being |
47 presently used for parsing/printing, see also isar-ref manual. |
47 presently used for parsing/printing, see also isar-ref manual. |
48 |
48 |
49 * Pure: tuned internal renaming of symbolic identifiers -- attach |
49 * Pure: tuned internal renaming of symbolic identifiers -- attach |
50 primes instead of base 26 numbers. |
50 primes instead of base 26 numbers. |
|
51 |
|
52 * Document preparation: antiquotations now provide the option |
|
53 'locale=NAME' to specify an alternative context used for evaluating |
|
54 and printing the subsequent argument, as in @{thm [locale=LC] |
|
55 fold_commute}, for example. Note that a proof context is escaped to |
|
56 the enclosing theory context first. |
51 |
57 |
52 * ML: all output via channels of writeln/warning/error etc. is now |
58 * ML: all output via channels of writeln/warning/error etc. is now |
53 passed through Output.output. This gives interface builders a |
59 passed through Output.output. This gives interface builders a |
54 chance to adapt text encodings in arbitrary manners (say as XML |
60 chance to adapt text encodings in arbitrary manners (say as XML |
55 entities); see the hook provided by Output.add_mode. On the other |
61 entities); see the hook provided by Output.add_mode. On the other |