equal
deleted
inserted
replaced
262 quotient_type spec' lthy |
262 quotient_type spec' lthy |
263 end |
263 end |
264 |
264 |
265 val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false |
265 val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false |
266 |
266 |
267 val quotspec_parser = |
|
268 Parse.and_list1 |
|
269 ((Parse.type_args -- Parse.binding) -- |
|
270 (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) |
|
271 Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- |
|
272 (@{keyword "/"} |-- (partial -- Parse.term)) -- |
|
273 Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))) |
|
274 |
|
275 val _ = |
267 val _ = |
276 Outer_Syntax.local_theory_to_proof "quotient_type" |
268 Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"} |
277 "quotient type definitions (require equivalence proofs)" |
269 "quotient type definitions (require equivalence proofs)" |
278 Keyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
270 (Parse.and_list1 |
|
271 ((Parse.type_args -- Parse.binding) -- |
|
272 (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) |
|
273 Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- |
|
274 (@{keyword "/"} |-- (partial -- Parse.term)) -- |
|
275 Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))) |
|
276 >> quotient_type_cmd) |
279 |
277 |
280 end; |
278 end; |