unfold_locales part of default method.

--- 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