equal
deleted
inserted
replaced
160 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
160 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
161 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
161 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
162 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
162 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
163 end |
163 end |
164 |
164 |
|
165 (* syntax setup *) |
|
166 local structure P = OuterParse in |
|
167 |
|
168 val quottype_parser = |
|
169 (P.type_args -- P.binding) -- |
|
170 P.opt_infix -- |
|
171 (P.$$$ "=" |-- P.term) -- |
|
172 (P.$$$ "/" |-- P.term) |
|
173 |
|
174 (* |
|
175 val _ = |
|
176 OuterSyntax.command "quotient" "quotient type definition (requires equivalence proof)" |
|
177 OuterKeyword.thy_goal |
|
178 (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); |
|
179 |
|
180 end; |
|
181 *) |
|
182 |
|
183 end; |
|
184 |
165 end; |
185 end; |
166 |
186 |
167 open Quotient |
187 open Quotient |