equal
deleted
inserted
replaced
341 |
341 |
342 \end{descr} |
342 \end{descr} |
343 |
343 |
344 Any goal statement causes some term abbreviations (such as |
344 Any goal statement causes some term abbreviations (such as |
345 \indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isacharquery}thesis}}}) to be bound automatically, see also |
345 \indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isacharquery}thesis}}}) to be bound automatically, see also |
346 \secref{sec:term-abbrev}. Furthermore, the local context of a |
346 \secref{sec:term-abbrev}. |
347 (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\hyperlink{case.rule-context}{\mbox{\isa{rule{\isacharunderscore}context}}} case. |
|
348 |
347 |
349 The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold |
348 The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold |
350 meaning: (1) during the of this claim they refer to the the local |
349 meaning: (1) during the of this claim they refer to the the local |
351 context introductions, (2) the resulting rule is annotated |
350 context introductions, (2) the resulting rule is annotated |
352 accordingly to support symbolic case splits when used with the |
351 accordingly to support symbolic case splits when used with the |