Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Sun, 01 Mar 2015 14:15:49 +0100
changeset 59572 7e4bf0824cd3
parent 59571 1081f91c0662
child 59573 d09cc83cdce9
tuned;
src/Doc/Implementation/ML.thy file | annotate | diff | comparison | revisions 
--- a/src/Doc/Implementation/ML.thy	Sat Feb 28 21:51:34 2015 +0100
+++ b/src/Doc/Implementation/ML.thy	Sun Mar 01 14:15:49 2015 +0100
@@ -1116,7 +1116,7 @@
 
   It is considered bad style to refer to internal function names or
   values in ML source notation in user error messages.  Do not use
-  @{text "@{make_string}"} here!
+  @{text "@{make_string}"} nor @{text "@{here}"}!
 
   Grammatical correctness of error messages can be improved by
   \emph{omitting} final punctuation: messages are often concatenated
isabelle