equal
deleted
inserted
replaced
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_class" "code_instance" "code_type" |
11 "export_code" "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 begin |
16 begin |
16 |
17 |
17 ML_file "~~/src/Tools/value.ML" |
18 ML_file "~~/src/Tools/value.ML" |
18 ML_file "~~/src/Tools/cache_io.ML" |
19 ML_file "~~/src/Tools/cache_io.ML" |
19 ML_file "~~/src/Tools/Code/code_preproc.ML" |
20 ML_file "~~/src/Tools/Code/code_preproc.ML" |