--- 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.
--- 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.
--- 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
--- 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