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/Logic.thy
changeset 47498 e3fc50c7da13
parent 47174 b9b2e183e94d 
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Mon Apr 16 21:37:08 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Mon Apr 16 21:53:11 2012 +0200
@@ -1123,7 +1123,10 @@
   1"}.  By working from right to left, newly emerging premises are
   concatenated in the result, without interfering.
 
-  \item @{text "rule OF rules"} abbreviates @{text "rules MRS rule"}.
+  \item @{text "rule OF rules"} is an alternative notation for @{text
+  "rules MRS rule"}, which makes rule composition look more like
+  function application.  Note that the argument @{text "rules"} need
+  not be atomic.
 
   This corresponds to the rule attribute @{attribute OF} in Isar
   source language.
isabelle