equal
deleted
inserted
replaced
176 end |
176 end |
177 in |
177 in |
178 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
178 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
179 end |
179 end |
180 |
180 |
|
181 (* FIXME: allow more than one type definition *) |
181 val quottype_parser = |
182 val quottype_parser = |
182 P.short_ident -- P.opt_infix -- |
183 P.short_ident -- P.opt_infix -- |
183 (P.$$$ "=" |-- P.typ) -- |
184 (P.$$$ "=" |-- P.typ) -- |
184 (P.$$$ "/" |-- P.term) |
185 (P.$$$ "/" |-- P.term) |
185 |
186 |
194 |
195 |
195 val _ = OuterKeyword.keyword "/" |
196 val _ = OuterKeyword.keyword "/" |
196 |
197 |
197 val _ = |
198 val _ = |
198 OuterSyntax.local_theory_to_proof "quotient" |
199 OuterSyntax.local_theory_to_proof "quotient" |
199 "quotient type definition (requires equivalence proof)" |
200 "quotient type definitions (requires equivalence proofs)" |
200 OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd) |
201 OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd) |
201 |
202 |
202 end; (* local *) |
203 end; (* local *) |
203 |
204 |
204 end; (* structure *) |
205 end; (* structure *) |