tuned comment;
authorwenzelm
Tue, 09 Apr 2013 13:20:09 +0200
changeset 51655 28d6eb23522c
parent 51654 8450b944e58a
child 51656 4ce2f7607d3d
tuned comment;
src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Tue Apr 09 12:56:26 2013 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Tue Apr 09 13:20:09 2013 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/Syntax/local_syntax.ML
     Author:     Makarius
 
-Local syntax depending on theory syntax.
+Local syntax depending on theory syntax, with special support for
+implicit structure references.
 *)
 
 signature LOCAL_SYNTAX =