# HG changeset patch
# User wenzelm
# Date 1116868456 -7200
# Node ID b6a945f205b720f46f193095b17d6674d00d7fc4
# Parent  828fc32f390f808671e95868c8182684c81e924f
* Pure/Syntax: In schematic variable names, *any* symbol following
  \<^isub> or \<^isup> is now treated as part of the base name;

diff -r 828fc32f390f -r b6a945f205b7 NEWS
--- a/NEWS	Mon May 23 17:17:06 2005 +0200
+++ b/NEWS	Mon May 23 19:14:16 2005 +0200
@@ -104,6 +104,13 @@
   matching the current goal as introduction rule and not having "HOL." 
   in their name (i.e. not being defined in theory HOL).
 
+* Pure/Syntax: In schematic variable names, *any* symbol following
+  \<^isub> or \<^isup> is now treated as part of the base name.  For
+  example, the following works without printing of ugly ".0" indexes:
+
+    lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1"
+      by simp
+
 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
 
 * Pure/Syntax: pretty pinter now supports unbreakable blocks,