32 \verb|bool|, \verb|int|, \verb|real|, or \verb|string|. Tools may declare options in ML, and then refer to these |
32 \verb|bool|, \verb|int|, \verb|real|, or \verb|string|. Tools may declare options in ML, and then refer to these |
33 values (relative to the context). Thus global reference variables |
33 values (relative to the context). Thus global reference variables |
34 are easily avoided. The user may change the value of a |
34 are easily avoided. The user may change the value of a |
35 configuration option by means of an associated attribute of the same |
35 configuration option by means of an associated attribute of the same |
36 name. This form of context declaration works particularly well with |
36 name. This form of context declaration works particularly well with |
37 commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}. |
37 commands such as \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} like |
38 |
38 this:% |
39 For historical reasons, some tools cannot take the full proof |
39 \end{isamarkuptext}% |
|
40 \isamarkuptrue% |
|
41 \isacommand{declare}\isamarkupfalse% |
|
42 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline |
|
43 \isanewline |
|
44 \isacommand{notepad}\isamarkupfalse% |
|
45 \isanewline |
|
46 \isakeyword{begin}\isanewline |
|
47 % |
|
48 \isadelimproof |
|
49 \ \ % |
|
50 \endisadelimproof |
|
51 % |
|
52 \isatagproof |
|
53 \isacommand{note}\isamarkupfalse% |
|
54 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal\ {\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}% |
|
55 \endisatagproof |
|
56 {\isafoldproof}% |
|
57 % |
|
58 \isadelimproof |
|
59 \isanewline |
|
60 % |
|
61 \endisadelimproof |
|
62 \isacommand{end}\isamarkupfalse% |
|
63 % |
|
64 \begin{isamarkuptext}% |
|
65 For historical reasons, some tools cannot take the full proof |
40 context into account and merely refer to the background theory. |
66 context into account and merely refer to the background theory. |
41 This is accommodated by configuration options being declared as |
67 This is accommodated by configuration options being declared as |
42 ``global'', which may not be changed within a local context. |
68 ``global'', which may not be changed within a local context. |
43 |
69 |
44 \begin{matharray}{rcll} |
70 \begin{matharray}{rcll} |