# HG changeset patch # User wenzelm # Date 1341584454 -7200 # Node ID 09c2a3d9aa22ebac4550cb7bfb17b5fa734921d6 # Parent 3155cee13c49e56ef003451e0102b8e7331acb15 discontinued obsolete attribute "COMP"; diff -r 3155cee13c49 -r 09c2a3d9aa22 NEWS --- 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 \ is now based on eurosym package, instead of diff -r 3155cee13c49 -r 09c2a3d9aa22 doc-src/IsarRef/Thy/Generic.thy --- 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 \ a\<^sub>n"} and @{attribute folded}~@{text "a\<^sub>1 \ a\<^sub>n"} expand and fold back again the given diff -r 3155cee13c49 -r 09c2a3d9aa22 doc-src/IsarRef/Thy/document/Generic.tex --- 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. diff -r 3155cee13c49 -r 09c2a3d9aa22 src/Pure/Isar/attrib.ML --- 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)