253 OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" |
253 OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" |
254 OuterKeyword.thy_goal |
254 OuterKeyword.thy_goal |
255 (Scan.optional (P.$$$ "(" |-- |
255 (Scan.optional (P.$$$ "(" |-- |
256 ((P.$$$ "open" >> K false) -- Scan.option P.binding || |
256 ((P.$$$ "open" >> K false) -- Scan.option P.binding || |
257 P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- |
257 P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- |
258 (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- |
258 (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- |
259 Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) |
259 Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) |
260 >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => |
260 >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => |
261 Toplevel.print o Toplevel.theory_to_proof |
261 Toplevel.print o Toplevel.theory_to_proof |
262 (typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs)))); |
262 (typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs)))); |
263 |
263 |