equal
deleted
inserted
replaced
379 \item [@{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}] |
379 \item [@{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}] |
380 reconsiders facts within a local context. Most notably, this may |
380 reconsiders facts within a local context. Most notably, this may |
381 include arbitrary declarations in any attribute specifications |
381 include arbitrary declarations in any attribute specifications |
382 included here, e.g.\ a local @{attribute simp} rule. |
382 included here, e.g.\ a local @{attribute simp} rule. |
383 |
383 |
384 \item [@{element "includes"}~@{text c}] copies the specified context |
384 The initial @{text import} specification of a locale |
385 in a statically scoped manner. Only available in the long goal |
|
386 format of \secref{sec:goals}. |
|
387 |
|
388 In contrast, the initial @{text import} specification of a locale |
|
389 expression maintains a dynamic relation to the locales being |
385 expression maintains a dynamic relation to the locales being |
390 referenced (benefiting from any later fact declarations in the |
386 referenced (benefiting from any later fact declarations in the |
391 obvious manner). |
387 obvious manner). |
392 |
388 |
393 \end{descr} |
389 \end{descr} |
431 repeatedly expand all introduction rules of locale predicates of the |
427 repeatedly expand all introduction rules of locale predicates of the |
432 theory. While @{method intro_locales} only applies the @{text |
428 theory. While @{method intro_locales} only applies the @{text |
433 loc.intro} introduction rules and therefore does not decend to |
429 loc.intro} introduction rules and therefore does not decend to |
434 assumptions, @{method unfold_locales} is more aggressive and applies |
430 assumptions, @{method unfold_locales} is more aggressive and applies |
435 @{text loc_axioms.intro} as well. Both methods are aware of locale |
431 @{text loc_axioms.intro} as well. Both methods are aware of locale |
436 specifications entailed by the context, both from target and |
432 specifications entailed by the context, both from target statements, |
437 @{element "includes"} statements, and from interpretations (see |
433 and from interpretations (see below). New goals that are entailed |
438 below). New goals that are entailed by the current context are |
434 by the current context are discharged automatically. |
439 discharged automatically. |
|
440 |
435 |
441 \end{descr} |
436 \end{descr} |
442 *} |
437 *} |
443 |
438 |
444 |
439 |