equal
deleted
inserted
replaced
300 end |
300 end |
301 |
301 |
302 val _ = OuterKeyword.keyword "/" |
302 val _ = OuterKeyword.keyword "/" |
303 |
303 |
304 val _ = |
304 val _ = |
305 OuterSyntax.local_theory_to_proof "quotient_type" |
305 OuterSyntax.local_theory_to_proof "quotient_type" |
306 "quotient type definitions (require equivalence proofs)" |
306 "quotient type definitions (require equivalence proofs)" |
307 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
307 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
308 |
308 |
309 end; (* structure *) |
309 end; (* structure *) |