src/Pure/Isar/ROOT.ML
changeset 24219 e558fe311376
parent 23896 26f92c405337
child 24306 7798a0f37253
equal deleted inserted replaced
24218:fbf1646b267c 24219:e558fe311376
    41 use "proof.ML";
    41 use "proof.ML";
    42 use "element.ML";
    42 use "element.ML";
    43 use "net_rules.ML";
    43 use "net_rules.ML";
    44 use "induct_attrib.ML";
    44 use "induct_attrib.ML";
    45 
    45 
    46 (*code generator base*)
    46 (*executable theory content*)
    47 use "../Tools/codegen_consts.ML";
    47 use "code_unit.ML";
    48 use "../Tools/codegen_func.ML";
    48 use "code.ML";
    49 use "../Tools/codegen_data.ML";
       
    50 
    49 
    51 (*derived theory and proof elements*)
    50 (*derived theory and proof elements*)
    52 use "local_theory.ML";
    51 use "local_theory.ML";
    53 use "calculation.ML";
    52 use "calculation.ML";
    54 use "obtain.ML";
    53 use "obtain.ML";
    55 use "locale.ML";
    54 use "locale.ML";
    56 use "spec_parse.ML";
    55 use "spec_parse.ML";
    57 use "../Tools/class_package.ML";
    56 use "class.ML";
    58 use "theory_target.ML";
    57 use "theory_target.ML";
    59 use "specification.ML";
    58 use "specification.ML";
    60 use "constdefs.ML";
    59 use "constdefs.ML";
    61 
    60 
    62 (*toplevel environment*)
    61 (*toplevel environment*)