equal
deleted
inserted
replaced
13 @{text "isabelle make"} |
13 @{text "isabelle make"} |
14 \end{center} |
14 \end{center} |
15 |
15 |
16 \item You can include references to other Isabelle manuals using the |
16 \item You can include references to other Isabelle manuals using the |
17 reference names from those manuals. To do this the following |
17 reference names from those manuals. To do this the following |
18 four latex commands are defined: |
18 four \LaTeX{} commands are defined: |
19 |
19 |
20 \begin{center} |
20 \begin{center} |
21 \begin{tabular}{l|c|c} |
21 \begin{tabular}{l|c|c} |
22 & Chapters & Sections\\\hline |
22 & Chapters & Sections\\\hline |
23 Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\ |
23 Implementation Manual & @{ML_text "\\ichcite{\<dots>}"} & @{ML_text "\\isccite{\<dots>}"}\\ |
42 ML-code. The @{text "for"} and @{text "in"} arguments are optional. The |
42 ML-code. The @{text "for"} and @{text "in"} arguments are optional. The |
43 former is used for evaluating open expressions by giving a list of |
43 former is used for evaluating open expressions by giving a list of |
44 free variables. The latter is used to indicate in which structure or structures the |
44 free variables. The latter is used to indicate in which structure or structures the |
45 ML-expression should be evaluated. Examples are: |
45 ML-expression should be evaluated. Examples are: |
46 |
46 |
47 \begin{center} |
47 \begin{center}\small |
48 \begin{tabular}{l} |
48 \begin{tabular}{l} |
49 @{text "@{ML \"1 + 3\"}"}\\ |
49 @{text "@{ML \"1 + 3\"}"}\\ |
50 @{text "@{ML \"a + b\" for a b}"}\\ |
50 @{text "@{ML \"a + b\" for a b}"}\\ |
51 @{text "@{ML Ident in OuterLex}"} |
51 @{text "@{ML Ident in OuterLex}"} |
52 \end{tabular} |
52 \end{tabular} |
65 |
65 |
66 \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like |
66 \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like |
67 the @{ML_text ML_response}-anti\-quotation, except that the |
67 the @{ML_text ML_response}-anti\-quotation, except that the |
68 result-specification is not checked. Use this antiquotation |
68 result-specification is not checked. Use this antiquotation |
69 if the result cannot be constructed or the code generates an exception. |
69 if the result cannot be constructed or the code generates an exception. |
|
70 |
|
71 \item[$\bullet$] @{text "@{ML_response_fake_both \"\<dots>\" \"\<dots>\"}"} can be |
|
72 used to show erroneous code. Neither the code nor the response will be |
|
73 chacked. |
70 |
74 |
71 \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when |
75 \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when |
72 referring to a file. It checks whether the file exists. |
76 referring to a file. It checks whether the file exists. |
73 \end{itemize} |
77 \end{itemize} |
74 |
78 |