changeset 70009 | 435fb018e8ee |
parent 69605 | a96320074298 |
--- a/src/Tools/Code_Generator.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/Tools/Code_Generator.thy Thu Mar 28 21:24:55 2019 +0100 @@ -11,7 +11,7 @@ "export_code" "code_identifier" "code_printing" "code_reserved" "code_monad" "code_reflect" :: thy_decl and "checking" and - "datatypes" "functions" "module_name" "file" + "datatypes" "functions" "module_name" "file" "file_prefix" "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module" :: quasi_command begin