equal
deleted
inserted
replaced
270 (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) |
270 (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) |
271 Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- |
271 Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- |
272 (Parse.$$$ "/" |-- (partial -- Parse.term)) -- |
272 (Parse.$$$ "/" |-- (partial -- Parse.term)) -- |
273 Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))) |
273 Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))) |
274 |
274 |
275 val _ = Keyword.keyword "/" |
|
276 |
|
277 val _ = |
275 val _ = |
278 Outer_Syntax.local_theory_to_proof "quotient_type" |
276 Outer_Syntax.local_theory_to_proof "quotient_type" |
279 "quotient type definitions (require equivalence proofs)" |
277 "quotient type definitions (require equivalence proofs)" |
280 Keyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
278 Keyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
281 |
279 |