1(*:maxLineLen=78:*) 2 3theory Isar 4imports Base 5begin 6 7chapter \<open>Isar language elements\<close> 8 9text \<open> 10 The Isar proof language (see also @{cite \<open>\S2\<close> "isabelle-isar-ref"}) 11 consists of three main categories of language elements: 12 13 \<^enum> Proof \<^emph>\<open>commands\<close> define the primary language of transactions of the 14 underlying Isar/VM interpreter. Typical examples are @{command "fix"}, 15 @{command "assume"}, @{command "show"}, @{command "proof"}, and @{command 16 "qed"}. 17 18 Composing proof commands according to the rules of the Isar/VM leads to 19 expressions of structured proof text, such that both the machine and the 20 human reader can give it a meaning as formal reasoning. 21 22 \<^enum> Proof \<^emph>\<open>methods\<close> define a secondary language of mixed forward-backward 23 refinement steps involving facts and goals. Typical examples are @{method 24 rule}, @{method unfold}, and @{method simp}. 25 26 Methods can occur in certain well-defined parts of the Isar proof language, 27 say as arguments to @{command "proof"}, @{command "qed"}, or @{command 28 "by"}. 29 30 \<^enum> \<^emph>\<open>Attributes\<close> define a tertiary language of small annotations to theorems 31 being defined or referenced. Attributes can modify both the context and the 32 theorem. 33 34 Typical examples are @{attribute intro} (which affects the context), and 35 @{attribute symmetric} (which affects the theorem). 36\<close> 37 38 39section \<open>Proof commands\<close> 40 41text \<open> 42 A \<^emph>\<open>proof command\<close> is state transition of the Isar/VM proof interpreter. 43 44 In principle, Isar proof commands could be defined in user-space as well. 45 The system is built like that in the first place: one part of the commands 46 are primitive, the other part is defined as derived elements. Adding to the 47 genuine structured proof language requires profound understanding of the 48 Isar/VM machinery, though, so this is beyond the scope of this manual. 49 50 What can be done realistically is to define some diagnostic commands that 51 inspect the general state of the Isar/VM, and report some feedback to the 52 user. Typically this involves checking of the linguistic \<^emph>\<open>mode\<close> of a proof 53 state, or peeking at the pending goals (if available). 54 55 Another common application is to define a toplevel command that poses a 56 problem to the user as Isar proof state and processes the final result 57 relatively to the context. Thus a proof can be incorporated into the context 58 of some user-space tool, without modifying the Isar proof language itself. 59\<close> 60 61text %mlref \<open> 62 \begin{mldecls} 63 @{index_ML_type Proof.state} \\ 64 @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\ 65 @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\ 66 @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\ 67 @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\ 68 @{index_ML Proof.goal: "Proof.state -> 69 {context: Proof.context, facts: thm list, goal: thm}"} \\ 70 @{index_ML Proof.raw_goal: "Proof.state -> 71 {context: Proof.context, facts: thm list, goal: thm}"} \\ 72 @{index_ML Proof.theorem: "Method.text option -> 73 (thm list list -> Proof.context -> Proof.context) -> 74 (term * term list) list list -> Proof.context -> Proof.state"} \\ 75 \end{mldecls} 76 77 \<^descr> Type @{ML_type Proof.state} represents Isar proof states. This is a 78 block-structured configuration with proof context, linguistic mode, and 79 optional goal. The latter consists of goal context, goal facts 80 (``\<open>using\<close>''), and tactical goal state (see \secref{sec:tactical-goals}). 81 82 The general idea is that the facts shall contribute to the refinement of 83 some parts of the tactical goal --- how exactly is defined by the proof 84 method that is applied in that situation. 85 86 \<^descr> @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML 87 Proof.assert_backward} are partial identity functions that fail unless a 88 certain linguistic mode is active, namely ``\<open>proof(state)\<close>'', 89 ``\<open>proof(chain)\<close>'', ``\<open>proof(prove)\<close>'', respectively (using the terminology 90 of @{cite "isabelle-isar-ref"}). 91 92 It is advisable study the implementations of existing proof commands for 93 suitable modes to be asserted. 94 95 \<^descr> @{ML Proof.simple_goal}~\<open>state\<close> returns the structured Isar goal (if 96 available) in the form seen by ``simple'' methods (like @{method simp} or 97 @{method blast}). The Isar goal facts are already inserted as premises into 98 the subgoals, which are presented individually as in @{ML Proof.goal}. 99 100 \<^descr> @{ML Proof.goal}~\<open>state\<close> returns the structured Isar goal (if available) 101 in the form seen by regular methods (like @{method rule}). The auxiliary 102 internal encoding of Pure conjunctions is split into individual subgoals as 103 usual. 104 105 \<^descr> @{ML Proof.raw_goal}~\<open>state\<close> returns the structured Isar goal (if 106 available) in the raw internal form seen by ``raw'' methods (like @{method 107 induct}). This form is rarely appropriate for diagnostic tools; @{ML 108 Proof.simple_goal} or @{ML Proof.goal} should be used in most situations. 109 110 \<^descr> @{ML Proof.theorem}~\<open>before_qed after_qed statement ctxt\<close> initializes a 111 toplevel Isar proof state within a given context. 112 113 The optional \<open>before_qed\<close> method is applied at the end of the proof, just 114 before extracting the result (this feature is rarely used). 115 116 The \<open>after_qed\<close> continuation receives the extracted result in order to apply 117 it to the final context in a suitable way (e.g.\ storing named facts). Note 118 that at this generic level the target context is specified as @{ML_type 119 Proof.context}, but the usual wrapping of toplevel proofs into command 120 transactions will provide a @{ML_type local_theory} here 121 (\chref{ch:local-theory}). This affects the way how results are stored. 122 123 The \<open>statement\<close> is given as a nested list of terms, each associated with 124 optional @{keyword "is"} patterns as usual in the Isar source language. The 125 original nested list structure over terms is turned into one over theorems 126 when \<open>after_qed\<close> is invoked. 127\<close> 128 129 130text %mlantiq \<open> 131 \begin{matharray}{rcl} 132 @{ML_antiquotation_def "Isar.goal"} & : & \<open>ML_antiquotation\<close> \\ 133 \end{matharray} 134 135 \<^descr> \<open>@{Isar.goal}\<close> refers to the regular goal state (if available) of the 136 current proof state managed by the Isar toplevel --- as abstract value. 137 138 This only works for diagnostic ML commands, such as @{command ML_val} or 139 @{command ML_command}. 140\<close> 141 142text %mlex \<open> 143 The following example peeks at a certain goal configuration. 144\<close> 145 146notepad 147begin 148 have A and B and C 149 ML_val 150 \<open>val n = Thm.nprems_of (#goal @{Isar.goal}); 151 @{assert} (n = 3);\<close> 152 sorry 153end 154 155text \<open> 156 Here we see 3 individual subgoals in the same way as regular proof methods 157 would do. 158\<close> 159 160 161section \<open>Proof methods\<close> 162 163text \<open> 164 A \<open>method\<close> is a function \<open>thm\<^sup>* \<rightarrow> context * goal \<rightarrow> (context \<times> goal)\<^sup>*\<^sup>*\<close> 165 that operates on the full Isar goal configuration with context, goal facts, 166 and tactical goal state and enumerates possible follow-up goal states. Under 167 normal circumstances, the goal context remains unchanged, but it is also 168 possible to declare named extensions of the proof context (\<^emph>\<open>cases\<close>). 169 170 This means a proof method is like a structurally enhanced tactic (cf.\ 171 \secref{sec:tactics}). The well-formedness conditions for tactics need to 172 hold for methods accordingly, with the following additions. 173 174 \<^item> Goal addressing is further limited either to operate uniformly on \<^emph>\<open>all\<close> 175 subgoals, or specifically on the \<^emph>\<open>first\<close> subgoal. 176 177 Exception: old-style tactic emulations that are embedded into the method 178 space, e.g.\ @{method rule_tac}. 179 180 \<^item> A non-trivial method always needs to make progress: an identical follow-up 181 goal state has to be avoided.\<^footnote>\<open>This enables the user to write method 182 expressions like \<open>meth\<^sup>+\<close> without looping, while the trivial do-nothing case 183 can be recovered via \<open>meth\<^sup>?\<close>.\<close> 184 185 Exception: trivial stuttering steps, such as ``@{method -}'' or @{method 186 succeed}. 187 188 \<^item> Goal facts passed to the method must not be ignored. If there is no 189 sensible use of facts outside the goal state, facts should be inserted into 190 the subgoals that are addressed by the method. 191 192 193 \<^medskip> 194 Syntactically, the language of proof methods appears as arguments to Isar 195 commands like @{command "by"} or @{command apply}. User-space additions are 196 reasonably easy by plugging suitable method-valued parser functions into the 197 framework, using the @{command method_setup} command, for example. 198 199 To get a better idea about the range of possibilities, consider the 200 following Isar proof schemes. This is the general form of structured proof 201 text: 202 203 \<^medskip> 204 \begin{tabular}{l} 205 @{command from}~\<open>facts\<^sub>1\<close>~@{command have}~\<open>props\<close>~@{command using}~\<open>facts\<^sub>2\<close> \\ 206 @{command proof}~\<open>(initial_method)\<close> \\ 207 \quad\<open>body\<close> \\ 208 @{command qed}~\<open>(terminal_method)\<close> \\ 209 \end{tabular} 210 \<^medskip> 211 212 The goal configuration consists of \<open>facts\<^sub>1\<close> and \<open>facts\<^sub>2\<close> appended in that 213 order, and various \<open>props\<close> being claimed. The \<open>initial_method\<close> is invoked 214 with facts and goals together and refines the problem to something that is 215 handled recursively in the proof \<open>body\<close>. The \<open>terminal_method\<close> has another 216 chance to finish any remaining subgoals, but it does not see the facts of 217 the initial step. 218 219 \<^medskip> 220 This pattern illustrates unstructured proof scripts: 221 222 \<^medskip> 223 \begin{tabular}{l} 224 @{command have}~\<open>props\<close> \\ 225 \quad@{command using}~\<open>facts\<^sub>1\<close>~@{command apply}~\<open>method\<^sub>1\<close> \\ 226 \quad@{command apply}~\<open>method\<^sub>2\<close> \\ 227 \quad@{command using}~\<open>facts\<^sub>3\<close>~@{command apply}~\<open>method\<^sub>3\<close> \\ 228 \quad@{command done} \\ 229 \end{tabular} 230 \<^medskip> 231 232 The \<open>method\<^sub>1\<close> operates on the original claim while using \<open>facts\<^sub>1\<close>. Since 233 the @{command apply} command structurally resets the facts, the \<open>method\<^sub>2\<close> 234 will operate on the remaining goal state without facts. The \<open>method\<^sub>3\<close> will 235 see again a collection of \<open>facts\<^sub>3\<close> that has been inserted into the script 236 explicitly. 237 238 \<^medskip> 239 Empirically, any Isar proof method can be categorized as follows. 240 241 \<^enum> \<^emph>\<open>Special method with cases\<close> with named context additions associated 242 with the follow-up goal state. 243 244 Example: @{method "induct"}, which is also a ``raw'' method since it 245 operates on the internal representation of simultaneous claims as Pure 246 conjunction (\secref{sec:logic-aux}), instead of separate subgoals 247 (\secref{sec:tactical-goals}). 248 249 \<^enum> \<^emph>\<open>Structured method\<close> with strong emphasis on facts outside the goal 250 state. 251 252 Example: @{method "rule"}, which captures the key ideas behind structured 253 reasoning in Isar in its purest form. 254 255 \<^enum> \<^emph>\<open>Simple method\<close> with weaker emphasis on facts, which are inserted into 256 subgoals to emulate old-style tactical ``premises''. 257 258 Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}. 259 260 \<^enum> \<^emph>\<open>Old-style tactic emulation\<close> with detailed numeric goal addressing and 261 explicit references to entities of the internal goal state (which are 262 otherwise invisible from proper Isar proof text). The naming convention 263 \<open>foo_tac\<close> makes this special non-standard status clear. 264 265 Example: @{method "rule_tac"}. 266 267 When implementing proof methods, it is advisable to study existing 268 implementations carefully and imitate the typical ``boiler plate'' for 269 context-sensitive parsing and further combinators to wrap-up tactic 270 expressions as methods.\<^footnote>\<open>Aliases or abbreviations of the standard method 271 combinators should be avoided. Note that from Isabelle99 until Isabelle2009 272 the system did provide various odd combinations of method syntax wrappers 273 that made applications more complicated than necessary.\<close> 274\<close> 275 276text %mlref \<open> 277 \begin{mldecls} 278 @{index_ML_type Proof.method} \\ 279 @{index_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\ 280 @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\ 281 @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\ 282 @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\ 283 @{index_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\ 284 @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser -> 285 string -> theory -> theory"} \\ 286 \end{mldecls} 287 288 \<^descr> Type @{ML_type Proof.method} represents proof methods as abstract type. 289 290 \<^descr> @{ML CONTEXT_METHOD}~\<open>(fn facts => context_tactic)\<close> wraps \<open>context_tactic\<close> 291 depending on goal facts as a general proof method that may change the proof 292 context dynamically. A typical operation is @{ML 293 Proof_Context.update_cases}, which is wrapped up as combinator @{index_ML 294 CONTEXT_CASES} for convenience. 295 296 \<^descr> @{ML METHOD}~\<open>(fn facts => tactic)\<close> wraps \<open>tactic\<close> depending on goal facts 297 as regular proof method; the goal context is passed via method syntax. 298 299 \<^descr> @{ML SIMPLE_METHOD}~\<open>tactic\<close> wraps a tactic that addresses all subgoals 300 uniformly as simple proof method. Goal facts are already inserted into all 301 subgoals before \<open>tactic\<close> is applied. 302 303 \<^descr> @{ML SIMPLE_METHOD'}~\<open>tactic\<close> wraps a tactic that addresses a specific 304 subgoal as simple proof method that operates on subgoal 1. Goal facts are 305 inserted into the subgoal then the \<open>tactic\<close> is applied. 306 307 \<^descr> @{ML Method.insert_tac}~\<open>ctxt facts i\<close> inserts \<open>facts\<close> into subgoal \<open>i\<close>. 308 This is convenient to reproduce part of the @{ML SIMPLE_METHOD} or @{ML 309 SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example. 310 311 \<^descr> @{ML Method.setup}~\<open>name parser description\<close> provides the functionality of 312 the Isar command @{command method_setup} as ML function. 313\<close> 314 315text %mlex \<open> 316 See also @{command method_setup} in @{cite "isabelle-isar-ref"} which 317 includes some abstract examples. 318 319 \<^medskip> 320 The following toy examples illustrate how the goal facts and state are 321 passed to proof methods. The predefined proof method called ``@{method 322 tactic}'' wraps ML source of type @{ML_type tactic} (abstracted over 323 @{ML_text facts}). This allows immediate experimentation without parsing of 324 concrete syntax. 325\<close> 326 327notepad 328begin 329 fix A B :: bool 330 assume a: A and b: B 331 332 have "A \<and> B" 333 apply (tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>) 334 using a apply (tactic \<open>resolve_tac @{context} facts 1\<close>) 335 using b apply (tactic \<open>resolve_tac @{context} facts 1\<close>) 336 done 337 338 have "A \<and> B" 339 using a and b 340 ML_val \<open>@{Isar.goal}\<close> 341 apply (tactic \<open>Method.insert_tac @{context} facts 1\<close>) 342 apply (tactic \<open>(resolve_tac @{context} @{thms conjI} THEN_ALL_NEW assume_tac @{context}) 1\<close>) 343 done 344end 345 346text \<open> 347 \<^medskip> 348 The next example implements a method that simplifies the first subgoal by 349 rewrite rules that are given as arguments. 350\<close> 351 352method_setup my_simp = 353 \<open>Attrib.thms >> (fn thms => fn ctxt => 354 SIMPLE_METHOD' (fn i => 355 CHANGED (asm_full_simp_tac 356 (put_simpset HOL_basic_ss ctxt addsimps thms) i)))\<close> 357 "rewrite subgoal by given rules" 358 359text \<open> 360 The concrete syntax wrapping of @{command method_setup} always 361 passes-through the proof context at the end of parsing, but it is not used 362 in this example. 363 364 The @{ML Attrib.thms} parser produces a list of theorems from the usual Isar 365 syntax involving attribute expressions etc.\ (syntax category @{syntax 366 thms}) @{cite "isabelle-isar-ref"}. The resulting @{ML_text thms} are 367 added to @{ML HOL_basic_ss} which already contains the basic Simplifier 368 setup for HOL. 369 370 The tactic @{ML asm_full_simp_tac} is the one that is also used in method 371 @{method simp} by default. The extra wrapping by the @{ML CHANGED} tactical 372 ensures progress of simplification: identical goal states are filtered out 373 explicitly to make the raw tactic conform to standard Isar method behaviour. 374 375 \<^medskip> 376 Method @{method my_simp} can be used in Isar proofs like this: 377\<close> 378 379notepad 380begin 381 fix a b c :: 'a 382 assume a: "a = b" 383 assume b: "b = c" 384 have "a = c" by (my_simp a b) 385end 386 387text \<open> 388 Here is a similar method that operates on all subgoals, instead of just the 389 first one.\<close> 390 391method_setup my_simp_all = 392 \<open>Attrib.thms >> (fn thms => fn ctxt => 393 SIMPLE_METHOD 394 (CHANGED 395 (ALLGOALS (asm_full_simp_tac 396 (put_simpset HOL_basic_ss ctxt addsimps thms)))))\<close> 397 "rewrite all subgoals by given rules" 398 399notepad 400begin 401 fix a b c :: 'a 402 assume a: "a = b" 403 assume b: "b = c" 404 have "a = c" and "c = b" by (my_simp_all a b) 405end 406 407text \<open> 408 \<^medskip> 409 Apart from explicit arguments, common proof methods typically work with a 410 default configuration provided by the context. As a shortcut to rule 411 management we use a cheap solution via the @{command named_theorems} command 412 to declare a dynamic fact in the context. 413\<close> 414 415named_theorems my_simp 416 417text \<open> 418 The proof method is now defined as before, but we append the explicit 419 arguments and the rules from the context. 420\<close> 421 422method_setup my_simp' = 423 \<open>Attrib.thms >> (fn thms => fn ctxt => 424 let 425 val my_simps = Named_Theorems.get ctxt @{named_theorems my_simp} 426 in 427 SIMPLE_METHOD' (fn i => 428 CHANGED (asm_full_simp_tac 429 (put_simpset HOL_basic_ss ctxt 430 addsimps (thms @ my_simps)) i)) 431 end)\<close> 432 "rewrite subgoal by given rules and my_simp rules from the context" 433 434text \<open> 435 \<^medskip> 436 Method @{method my_simp'} can be used in Isar proofs like this: 437\<close> 438 439notepad 440begin 441 fix a b c :: 'a 442 assume [my_simp]: "a \<equiv> b" 443 assume [my_simp]: "b \<equiv> c" 444 have "a \<equiv> c" by my_simp' 445end 446 447text \<open> 448 \<^medskip> 449 The @{method my_simp} variants defined above are ``simple'' methods, i.e.\ 450 the goal facts are merely inserted as goal premises by the @{ML 451 SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper. For proof methods that are 452 similar to the standard collection of @{method simp}, @{method blast}, 453 @{method fast}, @{method auto} there is little more that can be done. 454 455 Note that using the primary goal facts in the same manner as the method 456 arguments obtained via concrete syntax or the context does not meet the 457 requirement of ``strong emphasis on facts'' of regular proof methods, 458 because rewrite rules as used above can be easily ignored. A proof text 459 ``@{command using}~\<open>foo\<close>~@{command "by"}~\<open>my_simp\<close>'' where \<open>foo\<close> is not used 460 would deceive the reader. 461 462 \<^medskip> 463 The technical treatment of rules from the context requires further 464 attention. Above we rebuild a fresh @{ML_type simpset} from the arguments 465 and \<^emph>\<open>all\<close> rules retrieved from the context on every invocation of the 466 method. This does not scale to really large collections of rules, which 467 easily emerges in the context of a big theory library, for example. 468 469 This is an inherent limitation of the simplistic rule management via 470 @{command named_theorems}, because it lacks tool-specific storage and 471 retrieval. More realistic applications require efficient index-structures 472 that organize theorems in a customized manner, such as a discrimination net 473 that is indexed by the left-hand sides of rewrite rules. For variations on 474 the Simplifier, re-use of the existing type @{ML_type simpset} is adequate, 475 but scalability would require it be maintained statically within the context 476 data, not dynamically on each tool invocation. 477\<close> 478 479 480section \<open>Attributes \label{sec:attributes}\<close> 481 482text \<open> 483 An \<^emph>\<open>attribute\<close> is a function \<open>context \<times> thm \<rightarrow> context \<times> thm\<close>, which means 484 both a (generic) context and a theorem can be modified simultaneously. In 485 practice this mixed form is very rare, instead attributes are presented 486 either as \<^emph>\<open>declaration attribute:\<close> \<open>thm \<rightarrow> context \<rightarrow> context\<close> or \<^emph>\<open>rule 487 attribute:\<close> \<open>context \<rightarrow> thm \<rightarrow> thm\<close>. 488 489 Attributes can have additional arguments via concrete syntax. There is a 490 collection of context-sensitive parsers for various logical entities (types, 491 terms, theorems). These already take care of applying morphisms to the 492 arguments when attribute expressions are moved into a different context (see 493 also \secref{sec:morphisms}). 494 495 When implementing declaration attributes, it is important to operate exactly 496 on the variant of the generic context that is provided by the system, which 497 is either global theory context or local proof context. In particular, the 498 background theory of a local context must not be modified in this 499 situation! 500\<close> 501 502text %mlref \<open> 503 \begin{mldecls} 504 @{index_ML_type attribute} \\ 505 @{index_ML Thm.rule_attribute: "thm list -> 506 (Context.generic -> thm -> thm) -> attribute"} \\ 507 @{index_ML Thm.declaration_attribute: " 508 (thm -> Context.generic -> Context.generic) -> attribute"} \\ 509 @{index_ML Attrib.setup: "binding -> attribute context_parser -> 510 string -> theory -> theory"} \\ 511 \end{mldecls} 512 513 \<^descr> Type @{ML_type attribute} represents attributes as concrete type alias. 514 515 \<^descr> @{ML Thm.rule_attribute}~\<open>thms (fn context => rule)\<close> wraps a 516 context-dependent rule (mapping on @{ML_type thm}) as attribute. 517 518 The \<open>thms\<close> are additional parameters: when forming an abstract closure, the 519 system may provide dummy facts that are propagated according to strict 520 evaluation discipline. In that case, \<open>rule\<close> is bypassed. 521 522 \<^descr> @{ML Thm.declaration_attribute}~\<open>(fn thm => decl)\<close> wraps a 523 theorem-dependent declaration (mapping on @{ML_type Context.generic}) as 524 attribute. 525 526 When forming an abstract closure, the system may provide a dummy fact as 527 \<open>thm\<close>. In that case, \<open>decl\<close> is bypassed. 528 529 \<^descr> @{ML Attrib.setup}~\<open>name parser description\<close> provides the functionality of 530 the Isar command @{command attribute_setup} as ML function. 531\<close> 532 533text %mlantiq \<open> 534 \begin{matharray}{rcl} 535 @{ML_antiquotation_def attributes} & : & \<open>ML_antiquotation\<close> \\ 536 \end{matharray} 537 538 @{rail \<open> 539 @@{ML_antiquotation attributes} attributes 540 \<close>} 541 542 \<^descr> \<open>@{attributes [\<dots>]}\<close> embeds attribute source representation into the ML 543 text, which is particularly useful with declarations like @{ML 544 Local_Theory.note}. Attribute names are internalized at compile time, but 545 the source is unevaluated. This means attributes with formal arguments 546 (types, terms, theorems) may be subject to odd effects of dynamic scoping! 547\<close> 548 549text %mlex \<open> 550 See also @{command attribute_setup} in @{cite "isabelle-isar-ref"} which 551 includes some abstract examples. 552\<close> 553 554end 555