src/Tools/Code_Generator.thy
changeset 52138 e21426f244aa
parent 52137 7f7337447b1b
child 54890 cb892d835803
equal deleted inserted replaced
52137:7f7337447b1b 52138:e21426f244aa
     6 
     6 
     7 theory Code_Generator
     7 theory Code_Generator
     8 imports Pure
     8 imports Pure
     9 keywords
     9 keywords
    10   "value" "print_codeproc" "code_thms" "code_deps" :: diag and
    10   "value" "print_codeproc" "code_thms" "code_deps" :: diag and
    11   "export_code" "code_printing" "code_class" "code_instance" "code_type"
    11   "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type"
    12     "code_const" "code_reserved" "code_include" "code_modulename"
    12     "code_const" "code_reserved" "code_include" "code_modulename"
    13     "code_abort" "code_monad" "code_reflect" :: thy_decl and
    13     "code_abort" "code_monad" "code_reflect" :: thy_decl and
    14   "datatypes" "functions" "module_name" "file" "checking"
    14   "datatypes" "functions" "module_name" "file" "checking"
    15   "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
    15   "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
    16 begin
    16 begin