equal
deleted
inserted
replaced
50 primes instead of base 26 numbers. |
50 primes instead of base 26 numbers. |
51 |
51 |
52 * Document preparation: antiquotations now provide the option |
52 * Document preparation: antiquotations now provide the option |
53 'locale=NAME' to specify an alternative context used for evaluating |
53 'locale=NAME' to specify an alternative context used for evaluating |
54 and printing the subsequent argument, as in @{thm [locale=LC] |
54 and printing the subsequent argument, as in @{thm [locale=LC] |
55 fold_commute}, for example. Note that a proof context is escaped to |
55 fold_commute}, for example. |
56 the enclosing theory context first. |
|
57 |
56 |
58 * ML: output via the Isabelle channels of writeln/warning/error |
57 * ML: output via the Isabelle channels of writeln/warning/error |
59 etc. is now passed through Output.output, with a hook for arbitrary |
58 etc. is now passed through Output.output, with a hook for arbitrary |
60 transformations depending on the print_mode (cf. Output.add_mode -- |
59 transformations depending on the print_mode (cf. Output.add_mode -- |
61 the first active mode that provides a output function wins). |
60 the first active mode that provides a output function wins). |