# HG changeset patch
# User wenzelm
# Date 1152731967 -7200
# Node ID 0c1ec587a5a8aabe4cc91ded16f44b1dd93b25c6
# Parent  0f7b7bfae82b53275e158f552ab3cae1d9b6ece2
* Isar: ":" (colon) is no longer a symbolic identifier character;

diff -r 0f7b7bfae82b -r 0c1ec587a5a8 NEWS
--- a/NEWS	Wed Jul 12 21:19:24 2006 +0200
+++ b/NEWS	Wed Jul 12 21:19:27 2006 +0200
@@ -85,6 +85,10 @@
   have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
   have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
 
+* Isar: ":" (colon) is no longer a symbolic identifier character in
+outer syntax.  Thus symbolic identifiers may be used without
+additional white space in declarations like this: ``assume *: A''.
+
 * Isar: 'print_facts' prints all local facts of the current context,
 both named and unnamed ones.