# HG changeset patch
# User ballarin
# Date 1209736144 -7200
# Node ID f2ea56490bfb80d159453ab46734217b08b088ab
# Parent  805eece49928242ecd0e664da4dd9945b28a934c
unfold_locales part of default method.

diff -r 805eece49928 -r f2ea56490bfb NEWS
--- 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