175 clash with new theory Quotient in Main HOL. |
175 clash with new theory Quotient in Main HOL. |
176 |
176 |
177 |
177 |
178 *** ML *** |
178 *** ML *** |
179 |
179 |
180 * Antiquotations for type classes: |
180 * Antiquotations for basic formal entities: |
181 |
181 |
182 @{class NAME} -- type class |
182 @{class NAME} -- type class |
183 @{class_syntax NAME} -- syntax representation of any of the above |
183 @{class_syntax NAME} -- syntax representation of the above |
184 |
184 |
185 * Antiquotations for type constructors: |
185 @{type_name NAME} -- logical type |
186 |
|
187 @{type_name NAME} -- logical type (as before) |
|
188 @{type_abbrev NAME} -- type abbreviation |
186 @{type_abbrev NAME} -- type abbreviation |
189 @{nonterminal NAME} -- type of concrete syntactic category |
187 @{nonterminal NAME} -- type of concrete syntactic category |
190 @{type_syntax NAME} -- syntax representation of any of the above |
188 @{type_syntax NAME} -- syntax representation of any of the above |
|
189 |
|
190 @{const_name NAME} -- logical constant (INCOMPATIBILITY) |
|
191 @{const_abbrev NAME} -- abbreviated constant |
|
192 @{const_syntax NAME} -- syntax representation of any of the above |
191 |
193 |
192 * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw |
194 * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw |
193 syntax constant (cf. 'syntax' command). |
195 syntax constant (cf. 'syntax' command). |
194 |
196 |
195 * Renamed old-style Drule.standard to Drule.export_without_context, to |
197 * Renamed old-style Drule.standard to Drule.export_without_context, to |