Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/IsarImplementation/Thy/document/Logic.tex
changeset 47498 e3fc50c7da13
parent 47174 b9b2e183e94d 
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Apr 16 21:37:08 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Apr 16 21:53:11 2012 +0200
@@ -1261,7 +1261,9 @@
   against premise \isa{i} of \isa{rule}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}}.  By working from right to left, newly emerging premises are
   concatenated in the result, without interfering.
 
-  \item \isa{rule\ OF\ rules} abbreviates \isa{rules\ MRS\ rule}.
+  \item \isa{rule\ OF\ rules} is an alternative notation for \isa{rules\ MRS\ rule}, which makes rule composition look more like
+  function application.  Note that the argument \isa{rules} need
+  not be atomic.
 
   This corresponds to the rule attribute \hyperlink{attribute.OF}{\mbox{\isa{OF}}} in Isar
   source language.
isabelle