equal
deleted
inserted
replaced
1305 local |
1305 local |
1306 |
1306 |
1307 val _ = |
1307 val _ = |
1308 Outer_Syntax.command @{command_keyword code_datatype} |
1308 Outer_Syntax.command @{command_keyword code_datatype} |
1309 "define set of code datatype constructors" |
1309 "define set of code datatype constructors" |
1310 (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd)); |
1310 (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd)); |
1311 |
1311 |
1312 in end\<close> |
1312 in end\<close> |
1313 |
1313 |
1314 |
1314 |
1315 subsection \<open>Extraction of programs from proofs\<close> |
1315 subsection \<open>Extraction of programs from proofs\<close> |