# HG changeset patch
# User wenzelm
# Date 1374956164 -7200
# Node ID 821ce370b7fc16e151dd50cd3f8501d15fe6bdd5
# Parent  49825ba687ce84da69208595668caf7d7d2e192d
avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;

diff -r 49825ba687ce -r 821ce370b7fc NEWS
--- a/NEWS	Sat Jul 27 21:50:30 2013 +0200
+++ b/NEWS	Sat Jul 27 22:16:04 2013 +0200
@@ -136,7 +136,7 @@
   - Only one fundamental fold combinator on finite set remains:
     Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b
     This is now identity on infinite sets.
-  - Locales (»mini packages«) for fundamental definitions with
+  - Locales ("mini packages") for fundamental definitions with
     Finite_Set.fold: folding, folding_idem.
   - Locales comm_monoid_set, semilattice_order_set and
     semilattice_neutr_order_set for big operators on sets.