equal
deleted
inserted
replaced
395 \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] |
395 \item [\hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] |
396 reconsiders facts within a local context. Most notably, this may |
396 reconsiders facts within a local context. Most notably, this may |
397 include arbitrary declarations in any attribute specifications |
397 include arbitrary declarations in any attribute specifications |
398 included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule. |
398 included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule. |
399 |
399 |
400 \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context |
400 The initial \isa{import} specification of a locale |
401 in a statically scoped manner. Only available in the long goal |
|
402 format of \secref{sec:goals}. |
|
403 |
|
404 In contrast, the initial \isa{import} specification of a locale |
|
405 expression maintains a dynamic relation to the locales being |
401 expression maintains a dynamic relation to the locales being |
406 referenced (benefiting from any later fact declarations in the |
402 referenced (benefiting from any later fact declarations in the |
407 obvious manner). |
403 obvious manner). |
408 |
404 |
409 \end{descr} |
405 \end{descr} |
444 \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}] |
440 \item [\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}] |
445 repeatedly expand all introduction rules of locale predicates of the |
441 repeatedly expand all introduction rules of locale predicates of the |
446 theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to |
442 theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to |
447 assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies |
443 assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies |
448 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale |
444 \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale |
449 specifications entailed by the context, both from target and |
445 specifications entailed by the context, both from target statements, |
450 \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see |
446 and from interpretations (see below). New goals that are entailed |
451 below). New goals that are entailed by the current context are |
447 by the current context are discharged automatically. |
452 discharged automatically. |
|
453 |
448 |
454 \end{descr}% |
449 \end{descr}% |
455 \end{isamarkuptext}% |
450 \end{isamarkuptext}% |
456 \isamarkuptrue% |
451 \isamarkuptrue% |
457 % |
452 % |