# HG changeset patch
# User wenzelm
# Date 1334605991 -7200
# Node ID e3fc50c7da136bb5b3395ca672eef15d1347aa89
# Parent  c78c6e1ec75d35bcefd46e20e567638eb2667381
updated and clarified OF/MRS;

diff -r c78c6e1ec75d -r e3fc50c7da13 doc-src/IsarImplementation/Thy/Logic.thy
--- 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.
diff -r c78c6e1ec75d -r e3fc50c7da13 doc-src/IsarImplementation/Thy/document/Logic.tex
--- 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.
diff -r c78c6e1ec75d -r e3fc50c7da13 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 16 21:37:08 2012 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Apr 16 21:53:11 2012 +0200
@@ -784,11 +784,17 @@
   \item @{attribute (Pure) rule}~@{text del} undeclares introduction,
   elimination, or destruct rules.
   
-  \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
-  theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
-  (in parallel).  This corresponds to the @{ML_op "MRS"} operation in
-  ML, but note the reversed order.  Positions may be effectively
-  skipped by including ``@{text _}'' (underscore) as argument.
+  \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all
+  of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"} in canonical right-to-left
+  order, which means that premises stemming from the @{text "a\<^sub>i"}
+  emerge in parallel in the result, without interfering with each
+  other.  In many practical situations, the @{text "a\<^sub>i"} do not have
+  premises themselves, so @{text "rule [OF a\<^sub>1 \<dots> a\<^sub>n]"} can be actually
+  read as functional application (modulo unification).
+
+  Argument positions may be effectively skipped by using ``@{text _}''
+  (underscore), which refers to the propositional identity rule in the
+  Pure theory.
   
   \item @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
   instantiation of term variables.  The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
diff -r c78c6e1ec75d -r e3fc50c7da13 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 16 21:37:08 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Apr 16 21:53:11 2012 +0200
@@ -1111,11 +1111,17 @@
   \item \hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
   elimination, or destruct rules.
   
-  \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some
-  theorem to all of the given rules \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
-  (in parallel).  This corresponds to the \verb|MRS| operation in
-  ML, but note the reversed order.  Positions may be effectively
-  skipped by including ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'' (underscore) as argument.
+  \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some theorem to all
+  of the given rules \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} in canonical right-to-left
+  order, which means that premises stemming from the \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}}
+  emerge in parallel in the result, without interfering with each
+  other.  In many practical situations, the \isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} do not have
+  premises themselves, so \isa{{\isaliteral{22}{\isachardoublequote}}rule\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} can be actually
+  read as functional application (modulo unification).
+
+  Argument positions may be effectively skipped by using ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''
+  (underscore), which refers to the propositional identity rule in the
+  Pure theory.
   
   \item \hyperlink{attribute.of}{\mbox{\isa{of}}}~\isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} performs positional
   instantiation of term variables.  The terms \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are