| changeset 17228 | 19b460b39dad |
| parent 17193 | 83708f724822 |
| child 17259 | dda237f1d299 |
--- a/NEWS Thu Sep 01 23:08:15 2005 +0200 +++ b/NEWS Fri Sep 02 09:50:58 2005 +0200 @@ -261,6 +261,9 @@ alternative context used for evaluating and printing the subsequent argument, as in @{thm [locale=LC] fold_commute}, for example. +* Locale inspection command 'print_locale' omits notes elements. Use +'print_locale!' to have them included in the output. + *** Provers ***