* Isar: ":" (colon) is no longer a symbolic identifier character;
authorwenzelm
Wed, 12 Jul 2006 21:19:27 +0200
changeset 20118 0c1ec587a5a8
parent 20117 0f7b7bfae82b
child 20119 7923aacc10c6
* Isar: ":" (colon) is no longer a symbolic identifier character;
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.