changeset 26765 | f2ea56490bfb |
parent 26762 | 78ed28528ca6 |
child 26874 | b2daa27fc0a7 |
--- a/NEWS Fri May 02 02:17:07 2008 +0200 +++ b/NEWS Fri May 02 15:49:04 2008 +0200 @@ -98,6 +98,12 @@ situations. +*** Isar *** + +* Pure: default proof step now includes 'unfold_locales'; hence +'proof' without argument may be used to unfold locale predicates. + + *** Document preparation *** * Antiquotation "lemma" takes a proposition and a simple method text as argument