# HG changeset patch
# User wenzelm
# Date 1126728276 -7200
# Node ID 4dcae6e622680886be8ec79bca2298cab5905d51
# Parent  c01de5939f5b123ea06c00507f7afc6d08b8558e
HOL: method comm_ring;
Proof General: Unicode (UTF-8) support;

diff -r c01de5939f5b -r 4dcae6e62268 NEWS
--- a/NEWS	Wed Sep 14 22:04:35 2005 +0200
+++ b/NEWS	Wed Sep 14 22:04:36 2005 +0200
@@ -41,6 +41,11 @@
 matching the current goal as introduction rule and not having "HOL."
 in their name (i.e. not being defined in theory HOL).
 
+* Communication with Proof General is now 8bit clean, which means that
+Unicode text in UTF-8 encoding may be used within theory texts (both
+formal and informal parts).  See option -U of the Isabelle Proof
+General interface.
+
 
 *** Document preparation ***
 
@@ -224,29 +229,35 @@
 
 *** Locales ***
 
-* New commands for the interpretation of locale expressions in theories (1),
-locales (2) and proof contexts (3).  These generate proof obligations from
-the expression specification.  After the obligations have been discharged,
-theorems of the expression are added to the theory, target locale or proof
-context.  The synopsis of the commands is a follows:
+* New commands for the interpretation of locale expressions in
+theories (1), locales (2) and proof contexts (3).  These generate
+proof obligations from the expression specification.  After the
+obligations have been discharged, theorems of the expression are added
+to the theory, target locale or proof context.  The synopsis of the
+commands is a follows:
+
   (1) interpretation expr inst
   (2) interpretation target < expr
   (3) interpret expr inst
+
 Interpretation in theories and proof contexts require a parameter
 instantiation of terms from the current context.  This is applied to
-specifications and theorems of the interpreted expression.  Interpretation
-in locales only permits parameter renaming through the locale expression.
-Interpretation is smart in that interpretations that are active already
-do not occur in proof obligations, neither are instantiated theorems stored
-in duplicate.  Use 'print_interps' to inspect active interpretations of
-a particular locale.  For details, see the Isar Reference manual.
+specifications and theorems of the interpreted expression.
+Interpretation in locales only permits parameter renaming through the
+locale expression.  Interpretation is smart in that interpretations
+that are active already do not occur in proof obligations, neither are
+instantiated theorems stored in duplicate.  Use 'print_interps' to
+inspect active interpretations of a particular locale.  For details,
+see the Isar Reference manual.
 
 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
 'interpret' instead.
 
-* New context element 'constrains' for adding type constraints to parameters.
-
-* Context expressions: renaming of parameters with syntax redeclaration.
+* New context element 'constrains' for adding type constraints to
+parameters.
+
+* Context expressions: renaming of parameters with syntax
+redeclaration.
 
 * Locale declaration: 'includes' disallowed.