equal
deleted
inserted
replaced
217 (OuterParse.$$$ "/" |-- OuterParse.term)) |
217 (OuterParse.$$$ "/" |-- OuterParse.term)) |
218 |
218 |
219 val _ = OuterKeyword.keyword "/" |
219 val _ = OuterKeyword.keyword "/" |
220 |
220 |
221 val _ = |
221 val _ = |
222 OuterSyntax.local_theory_to_proof "quotient" |
222 OuterSyntax.local_theory_to_proof "quotient_type" |
223 "quotient type definitions (requires equivalence proofs)" |
223 "quotient type definitions (require equivalence proofs)" |
224 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
224 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
225 |
225 |
226 end; (* structure *) |
226 end; (* structure *) |
227 |
227 |
228 |
228 |