equal
deleted
inserted
replaced
478 |
478 |
479 val _ = |
479 val _ = |
480 OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl |
480 OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl |
481 (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); |
481 (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd)); |
482 |
482 |
483 val _ = |
|
484 OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal |
|
485 (P.term -- P.term >> (fn (abs, rep) => Toplevel.print |
|
486 o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep))); |
|
487 |
|
488 |
483 |
489 |
484 |
490 (** proof commands **) |
485 (** proof commands **) |
491 |
486 |
492 (* statements *) |
487 (* statements *) |