25 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
26 FIXME% |
26 FIXME% |
27 \end{isamarkuptext}% |
27 \end{isamarkuptext}% |
28 \isamarkuptrue% |
28 \isamarkuptrue% |
29 % |
29 % |
30 \isamarkupsection{Parsing and printing% |
30 \isamarkupsection{Reading and pretty printing \label{sec:read-print}% |
31 } |
31 } |
32 \isamarkuptrue% |
32 \isamarkuptrue% |
33 % |
33 % |
34 \begin{isamarkuptext}% |
34 \begin{isamarkuptext}% |
35 FIXME% |
35 FIXME% |
36 \end{isamarkuptext}% |
36 \end{isamarkuptext}% |
37 \isamarkuptrue% |
37 \isamarkuptrue% |
|
38 % |
|
39 \isadelimmlref |
|
40 % |
|
41 \endisadelimmlref |
|
42 % |
|
43 \isatagmlref |
|
44 % |
|
45 \begin{isamarkuptext}% |
|
46 \begin{mldecls} |
|
47 \indexdef{}{ML}{Syntax.read\_typ}\verb|Syntax.read_typ: Proof.context -> string -> typ| \\ |
|
48 \indexdef{}{ML}{Syntax.read\_term}\verb|Syntax.read_term: Proof.context -> string -> term| \\ |
|
49 \indexdef{}{ML}{Syntax.read\_prop}\verb|Syntax.read_prop: Proof.context -> string -> term| \\ |
|
50 \indexdef{}{ML}{Syntax.pretty\_typ}\verb|Syntax.pretty_typ: Proof.context -> typ -> Pretty.T| \\ |
|
51 \indexdef{}{ML}{Syntax.pretty\_term}\verb|Syntax.pretty_term: Proof.context -> term -> Pretty.T| \\ |
|
52 \end{mldecls} |
|
53 |
|
54 \begin{description} |
|
55 |
|
56 \item FIXME |
|
57 |
|
58 \end{description}% |
|
59 \end{isamarkuptext}% |
|
60 \isamarkuptrue% |
|
61 % |
|
62 \endisatagmlref |
|
63 {\isafoldmlref}% |
|
64 % |
|
65 \isadelimmlref |
|
66 % |
|
67 \endisadelimmlref |
|
68 % |
|
69 \isamarkupsection{Parsing and unparsing \label{sec:parse-unparse}% |
|
70 } |
|
71 \isamarkuptrue% |
|
72 % |
|
73 \begin{isamarkuptext}% |
|
74 FIXME% |
|
75 \end{isamarkuptext}% |
|
76 \isamarkuptrue% |
|
77 % |
|
78 \isadelimmlref |
|
79 % |
|
80 \endisadelimmlref |
|
81 % |
|
82 \isatagmlref |
|
83 % |
|
84 \begin{isamarkuptext}% |
|
85 \begin{mldecls} |
|
86 \indexdef{}{ML}{Syntax.parse\_typ}\verb|Syntax.parse_typ: Proof.context -> string -> typ| \\ |
|
87 \indexdef{}{ML}{Syntax.parse\_term}\verb|Syntax.parse_term: Proof.context -> string -> term| \\ |
|
88 \indexdef{}{ML}{Syntax.parse\_prop}\verb|Syntax.parse_prop: Proof.context -> string -> term| \\ |
|
89 \indexdef{}{ML}{Syntax.unparse\_typ}\verb|Syntax.unparse_typ: Proof.context -> typ -> Pretty.T| \\ |
|
90 \indexdef{}{ML}{Syntax.unparse\_term}\verb|Syntax.unparse_term: Proof.context -> term -> Pretty.T| \\ |
|
91 \end{mldecls} |
|
92 |
|
93 \begin{description} |
|
94 |
|
95 \item FIXME |
|
96 |
|
97 \end{description}% |
|
98 \end{isamarkuptext}% |
|
99 \isamarkuptrue% |
|
100 % |
|
101 \endisatagmlref |
|
102 {\isafoldmlref}% |
|
103 % |
|
104 \isadelimmlref |
|
105 % |
|
106 \endisadelimmlref |
38 % |
107 % |
39 \isamarkupsection{Checking and unchecking \label{sec:term-check}% |
108 \isamarkupsection{Checking and unchecking \label{sec:term-check}% |
40 } |
109 } |
41 \isamarkuptrue% |
110 \isamarkuptrue% |
|
111 % |
|
112 \begin{isamarkuptext}% |
|
113 FIXME% |
|
114 \end{isamarkuptext}% |
|
115 \isamarkuptrue% |
|
116 % |
|
117 \isadelimmlref |
|
118 % |
|
119 \endisadelimmlref |
|
120 % |
|
121 \isatagmlref |
|
122 % |
|
123 \begin{isamarkuptext}% |
|
124 \begin{mldecls} |
|
125 \indexdef{}{ML}{Syntax.check\_typs}\verb|Syntax.check_typs: Proof.context -> typ list -> typ list| \\ |
|
126 \indexdef{}{ML}{Syntax.check\_terms}\verb|Syntax.check_terms: Proof.context -> term list -> term list| \\ |
|
127 \indexdef{}{ML}{Syntax.check\_props}\verb|Syntax.check_props: Proof.context -> term list -> term list| \\ |
|
128 \indexdef{}{ML}{Syntax.uncheck\_typs}\verb|Syntax.uncheck_typs: Proof.context -> typ list -> typ list| \\ |
|
129 \indexdef{}{ML}{Syntax.uncheck\_terms}\verb|Syntax.uncheck_terms: Proof.context -> term list -> term list| \\ |
|
130 \end{mldecls} |
|
131 |
|
132 \begin{description} |
|
133 |
|
134 \item FIXME |
|
135 |
|
136 \end{description}% |
|
137 \end{isamarkuptext}% |
|
138 \isamarkuptrue% |
|
139 % |
|
140 \endisatagmlref |
|
141 {\isafoldmlref}% |
|
142 % |
|
143 \isadelimmlref |
|
144 % |
|
145 \endisadelimmlref |
|
146 % |
|
147 \isamarkupsection{Syntax translations% |
|
148 } |
|
149 \isamarkuptrue% |
|
150 % |
|
151 \begin{isamarkuptext}% |
|
152 FIXME% |
|
153 \end{isamarkuptext}% |
|
154 \isamarkuptrue% |
|
155 % |
|
156 \isadelimmlantiq |
|
157 % |
|
158 \endisadelimmlantiq |
|
159 % |
|
160 \isatagmlantiq |
|
161 % |
|
162 \begin{isamarkuptext}% |
|
163 \begin{matharray}{rcl} |
|
164 \indexdef{}{ML antiquotation}{class\_syntax}\hypertarget{ML antiquotation.class-syntax}{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isacharunderscore}syntax}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\ |
|
165 \indexdef{}{ML antiquotation}{type\_syntax}\hypertarget{ML antiquotation.type-syntax}{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isacharunderscore}syntax}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\ |
|
166 \indexdef{}{ML antiquotation}{const\_syntax}\hypertarget{ML antiquotation.const-syntax}{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isacharunderscore}syntax}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\ |
|
167 \indexdef{}{ML antiquotation}{syntax\_const}\hypertarget{ML antiquotation.syntax-const}{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isacharunderscore}const}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\ |
|
168 \end{matharray} |
|
169 |
|
170 \begin{rail} |
|
171 ('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name |
|
172 ; |
|
173 \end{rail} |
|
174 |
|
175 \begin{description} |
|
176 |
|
177 \item FIXME |
|
178 |
|
179 \end{description}% |
|
180 \end{isamarkuptext}% |
|
181 \isamarkuptrue% |
|
182 % |
|
183 \endisatagmlantiq |
|
184 {\isafoldmlantiq}% |
|
185 % |
|
186 \isadelimmlantiq |
|
187 % |
|
188 \endisadelimmlantiq |
42 % |
189 % |
43 \isadelimtheory |
190 \isadelimtheory |
44 % |
191 % |
45 \endisadelimtheory |
192 \endisadelimtheory |
46 % |
193 % |