[isabelle-dev] Unfold_locales

[Clemens Ballarin]

* Pure: default proof step now includes 'unfold_locales'; hence  
'proof' without argument may be used to unfold locale predicates.

Thanks to Florian for implementing this.

Clemens