125 |
125 |
126 \begin{matharray}{rcl} |
126 \begin{matharray}{rcl} |
127 @{attribute_def tagged} & : & @{text attribute} \\ |
127 @{attribute_def tagged} & : & @{text attribute} \\ |
128 @{attribute_def untagged} & : & @{text attribute} \\[0.5ex] |
128 @{attribute_def untagged} & : & @{text attribute} \\[0.5ex] |
129 @{attribute_def THEN} & : & @{text attribute} \\ |
129 @{attribute_def THEN} & : & @{text attribute} \\ |
130 @{attribute_def COMP} & : & @{text attribute} \\[0.5ex] |
|
131 @{attribute_def unfolded} & : & @{text attribute} \\ |
130 @{attribute_def unfolded} & : & @{text attribute} \\ |
132 @{attribute_def folded} & : & @{text attribute} \\ |
131 @{attribute_def folded} & : & @{text attribute} \\ |
133 @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex] |
132 @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex] |
134 @{attribute_def rotated} & : & @{text attribute} \\ |
133 @{attribute_def rotated} & : & @{text attribute} \\ |
135 @{attribute_def (Pure) elim_format} & : & @{text attribute} \\ |
134 @{attribute_def (Pure) elim_format} & : & @{text attribute} \\ |
140 @{rail " |
139 @{rail " |
141 @@{attribute tagged} @{syntax name} @{syntax name} |
140 @@{attribute tagged} @{syntax name} @{syntax name} |
142 ; |
141 ; |
143 @@{attribute untagged} @{syntax name} |
142 @@{attribute untagged} @{syntax name} |
144 ; |
143 ; |
145 (@@{attribute THEN} | @@{attribute COMP}) ('[' @{syntax nat} ']')? @{syntax thmref} |
144 @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref} |
146 ; |
145 ; |
147 (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs} |
146 (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs} |
148 ; |
147 ; |
149 @@{attribute rotated} @{syntax int}? |
148 @@{attribute rotated} @{syntax int}? |
150 "} |
149 "} |
155 untagged}~@{text name} add and remove \emph{tags} of some theorem. |
154 untagged}~@{text name} add and remove \emph{tags} of some theorem. |
156 Tags may be any list of string pairs that serve as formal comment. |
155 Tags may be any list of string pairs that serve as formal comment. |
157 The first string is considered the tag name, the second its value. |
156 The first string is considered the tag name, the second its value. |
158 Note that @{attribute untagged} removes any tags of the same name. |
157 Note that @{attribute untagged} removes any tags of the same name. |
159 |
158 |
160 \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a} |
159 \item @{attribute THEN}~@{text a} composes rules by resolution; it |
161 compose rules by resolution. @{attribute THEN} resolves with the |
160 resolves with the first premise of @{text a} (an alternative |
162 first premise of @{text a} (an alternative position may be also |
161 position may be also specified). See also @{ML_op "RS"} in |
163 specified); the @{attribute COMP} version skips the automatic |
162 \cite{isabelle-implementation}. |
164 lifting process that is normally intended (cf.\ @{ML_op "RS"} and |
|
165 @{ML_op "COMP"} in \cite{isabelle-implementation}). |
|
166 |
163 |
167 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute |
164 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute |
168 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given |
165 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given |
169 definitions throughout a rule. |
166 definitions throughout a rule. |
170 |
167 |