discontinued obsolete attribute "COMP";
authorwenzelm
Fri Jul 06 16:20:54 2012 +0200 (2012-07-06)
changeset 4820509c2a3d9aa22
parent 48204 3155cee13c49
child 48206 937b53a339f0
discontinued obsolete attribute "COMP";
NEWS
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/document/Generic.tex
src/Pure/Isar/attrib.ML
     1.1 --- a/NEWS	Thu Jul 05 22:17:57 2012 +0200
     1.2 +++ b/NEWS	Fri Jul 06 16:20:54 2012 +0200
     1.3 @@ -13,6 +13,15 @@
     1.4  in old "ref" manual.
     1.5  
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
    1.10 +use regular rule composition via "OF" / "THEN", or explicit proof
    1.11 +structure instead.  Note that Isabelle/ML provides a variety of
    1.12 +operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
    1.13 +with some care where this is really required.
    1.14 +
    1.15 +
    1.16  *** Document preparation ***
    1.17  
    1.18  * Default for \<euro> is now based on eurosym package, instead of
     2.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Thu Jul 05 22:17:57 2012 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Fri Jul 06 16:20:54 2012 +0200
     2.3 @@ -127,7 +127,6 @@
     2.4      @{attribute_def tagged} & : & @{text attribute} \\
     2.5      @{attribute_def untagged} & : & @{text attribute} \\[0.5ex]
     2.6      @{attribute_def THEN} & : & @{text attribute} \\
     2.7 -    @{attribute_def COMP} & : & @{text attribute} \\[0.5ex]
     2.8      @{attribute_def unfolded} & : & @{text attribute} \\
     2.9      @{attribute_def folded} & : & @{text attribute} \\
    2.10      @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
    2.11 @@ -142,7 +141,7 @@
    2.12      ;
    2.13      @@{attribute untagged} @{syntax name}
    2.14      ;
    2.15 -    (@@{attribute THEN} | @@{attribute COMP}) ('[' @{syntax nat} ']')? @{syntax thmref}
    2.16 +    @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
    2.17      ;
    2.18      (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
    2.19      ;
    2.20 @@ -157,12 +156,10 @@
    2.21    The first string is considered the tag name, the second its value.
    2.22    Note that @{attribute untagged} removes any tags of the same name.
    2.23  
    2.24 -  \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}
    2.25 -  compose rules by resolution.  @{attribute THEN} resolves with the
    2.26 -  first premise of @{text a} (an alternative position may be also
    2.27 -  specified); the @{attribute COMP} version skips the automatic
    2.28 -  lifting process that is normally intended (cf.\ @{ML_op "RS"} and
    2.29 -  @{ML_op "COMP"} in \cite{isabelle-implementation}).
    2.30 +  \item @{attribute THEN}~@{text a} composes rules by resolution; it
    2.31 +  resolves with the first premise of @{text a} (an alternative
    2.32 +  position may be also specified).  See also @{ML_op "RS"} in
    2.33 +  \cite{isabelle-implementation}.
    2.34    
    2.35    \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute
    2.36    folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given
     3.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu Jul 05 22:17:57 2012 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Fri Jul 06 16:20:54 2012 +0200
     3.3 @@ -215,7 +215,6 @@
     3.4      \indexdef{}{attribute}{tagged}\hypertarget{attribute.tagged}{\hyperlink{attribute.tagged}{\mbox{\isa{tagged}}}} & : & \isa{attribute} \\
     3.5      \indexdef{}{attribute}{untagged}\hypertarget{attribute.untagged}{\hyperlink{attribute.untagged}{\mbox{\isa{untagged}}}} & : & \isa{attribute} \\[0.5ex]
     3.6      \indexdef{}{attribute}{THEN}\hypertarget{attribute.THEN}{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}} & : & \isa{attribute} \\
     3.7 -    \indexdef{}{attribute}{COMP}\hypertarget{attribute.COMP}{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}} & : & \isa{attribute} \\[0.5ex]
     3.8      \indexdef{}{attribute}{unfolded}\hypertarget{attribute.unfolded}{\hyperlink{attribute.unfolded}{\mbox{\isa{unfolded}}}} & : & \isa{attribute} \\
     3.9      \indexdef{}{attribute}{folded}\hypertarget{attribute.folded}{\hyperlink{attribute.folded}{\mbox{\isa{folded}}}} & : & \isa{attribute} \\
    3.10      \indexdef{}{attribute}{abs\_def}\hypertarget{attribute.abs-def}{\hyperlink{attribute.abs-def}{\mbox{\isa{abs{\isaliteral{5F}{\isacharunderscore}}def}}}} & : & \isa{attribute} \\[0.5ex]
    3.11 @@ -236,11 +235,7 @@
    3.12  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    3.13  \rail@end
    3.14  \rail@begin{2}{}
    3.15 -\rail@bar
    3.16  \rail@term{\hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}}[]
    3.17 -\rail@nextbar{1}
    3.18 -\rail@term{\hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}}[]
    3.19 -\rail@endbar
    3.20  \rail@bar
    3.21  \rail@nextbar{1}
    3.22  \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
    3.23 @@ -274,12 +269,10 @@
    3.24    The first string is considered the tag name, the second its value.
    3.25    Note that \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} removes any tags of the same name.
    3.26  
    3.27 -  \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} and \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}}~\isa{a}
    3.28 -  compose rules by resolution.  \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} resolves with the
    3.29 -  first premise of \isa{a} (an alternative position may be also
    3.30 -  specified); the \hyperlink{attribute.COMP}{\mbox{\isa{COMP}}} version skips the automatic
    3.31 -  lifting process that is normally intended (cf.\ \verb|RS| and
    3.32 -  \verb|COMP| in \cite{isabelle-implementation}).
    3.33 +  \item \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}~\isa{a} composes rules by resolution; it
    3.34 +  resolves with the first premise of \isa{a} (an alternative
    3.35 +  position may be also specified).  See also \verb|RS| in
    3.36 +  \cite{isabelle-implementation}.
    3.37    
    3.38    \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
    3.39    definitions throughout a rule.
     4.1 --- a/src/Pure/Isar/attrib.ML	Thu Jul 05 22:17:57 2012 +0200
     4.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jul 06 16:20:54 2012 +0200
     4.3 @@ -320,10 +320,6 @@
     4.4  
     4.5  (* rule composition *)
     4.6  
     4.7 -val COMP_att =
     4.8 -  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
     4.9 -    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
    4.10 -
    4.11  val THEN_att =
    4.12    Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    4.13      >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
    4.14 @@ -388,7 +384,6 @@
    4.15    setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
    4.16    setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
    4.17    setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
    4.18 -  setup (Binding.name "COMP") COMP_att "direct composition with rules (no lifting)" #>
    4.19    setup (Binding.name "THEN") THEN_att "resolution with rule" #>
    4.20    setup (Binding.name "OF") OF_att "rule applied to facts" #>
    4.21    setup (Binding.name "rename_abs") (Scan.lift rename_abs)