--- a/NEWS Thu Jul 05 22:17:57 2012 +0200
+++ b/NEWS Fri Jul 06 16:20:54 2012 +0200
@@ -13,6 +13,15 @@
in old "ref" manual.
+*** Pure ***
+
+* Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY,
+use regular rule composition via "OF" / "THEN", or explicit proof
+structure instead. Note that Isabelle/ML provides a variety of
+operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
+with some care where this is really required.
+
+
*** Document preparation ***
* Default for \<euro> is now based on eurosym package, instead of
--- a/doc-src/IsarRef/Thy/Generic.thy Thu Jul 05 22:17:57 2012 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Fri Jul 06 16:20:54 2012 +0200
@@ -127,7 +127,6 @@
@{attribute_def tagged} & : & @{text attribute} \\
@{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
@{attribute_def THEN} & : & @{text attribute} \\
- @{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
@{attribute_def unfolded} & : & @{text attribute} \\
@{attribute_def folded} & : & @{text attribute} \\
@{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
@@ -142,7 +141,7 @@
;
@@{attribute untagged} @{syntax name}
;
- (@@{attribute THEN} | @@{attribute COMP}) ('[' @{syntax nat} ']')? @{syntax thmref}
+ @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
;
(@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
;
@@ -157,12 +156,10 @@
The first string is considered the tag name, the second its value.
Note that @{attribute untagged} removes any tags of the same name.
- \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}
- compose rules by resolution. @{attribute THEN} resolves with the
- first premise of @{text a} (an alternative position may be also
- specified); the @{attribute COMP} version skips the automatic
- lifting process that is normally intended (cf.\ @{ML_op "RS"} and
- @{ML_op "COMP"} in \cite{isabelle-implementation}).
+ \item @{attribute THEN}~@{text a} composes rules by resolution; it
+ resolves with the first premise of @{text a} (an alternative
+ position may be also specified). See also @{ML_op "RS"} in
+ \cite{isabelle-implementation}.
\item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
--- a/doc-src/IsarRef/Thy/document/Generic.tex Thu Jul 05 22:17:57 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Fri Jul 06 16:20:54 2012 +0200
@@ -215,7 +215,6 @@
\indexdef{}{attribute}{tagged}\hypertarget{attribute.tagged}{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}} & : & \isa{attribute} \\
\indexdef{}{attribute}{untagged}\hypertarget{attribute.untagged}{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}} & : & \isa{attribute} \\[0.5ex]
\indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isa{attribute} \\
- \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isa{attribute} \\[0.5ex]
\indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isa{attribute} \\
\indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\
\indexdef{}{attribute}{abs\_def}\hypertarget{attribute.abs-def}{\hyperlink{attribute.abs-def}{\mbox{\isa{abs{\isaliteral{5F}{\isacharunderscore}}def}}}} & : & \isa{attribute} \\[0.5ex]
@@ -236,11 +235,7 @@
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
\rail@begin{2}{}
-\rail@bar
\rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}}[]
-\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
@@ -274,12 +269,10 @@
The first string is considered the tag name, the second its value.
Note that \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} removes any tags of the same name.
- \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} and \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}~\isa{a}
- compose rules by resolution. \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
- first premise of \isa{a} (an alternative position may be also
- specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
- lifting process that is normally intended (cf.\ \verb|RS| and
- \verb|COMP| in \cite{isabelle-implementation}).
+ \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} composes rules by resolution; it
+ resolves with the first premise of \isa{a} (an alternative
+ position may be also specified). See also \verb|RS| in
+ \cite{isabelle-implementation}.
\item \hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} and \hyperlink{attribute.folded}{\mbox{\isa{folded}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} expand and fold back again the given
definitions throughout a rule.
--- a/src/Pure/Isar/attrib.ML Thu Jul 05 22:17:57 2012 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Jul 06 16:20:54 2012 +0200
@@ -320,10 +320,6 @@
(* rule composition *)
-val COMP_att =
- Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
- >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
-
val THEN_att =
Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
@@ -388,7 +384,6 @@
setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
- setup (Binding.name "COMP") COMP_att "direct composition with rules (no lifting)" #>
setup (Binding.name "THEN") THEN_att "resolution with rule" #>
setup (Binding.name "OF") OF_att "rule applied to facts" #>
setup (Binding.name "rename_abs") (Scan.lift rename_abs)