src/Pure/ROOT.ML
changeset 5834 c6fea8488ce7
parent 5684 9a3acc4c7c2e
child 6038 dfdb7584cf96
equal deleted inserted replaced
5833:6d8bceaa07b3 5834:c6fea8488ce7
     8 
     8 
     9 val banner = "Pure Isabelle";
     9 val banner = "Pure Isabelle";
    10 val version = "Isabelle repository";
    10 val version = "Isabelle repository";
    11 
    11 
    12 print_depth 1;
    12 print_depth 1;
    13 ml_prompts "> " "# ";
       
    14 
    13 
    15 (*fake hiding of private structures*)
    14 (*fake hiding of private structures*)
    16 structure Hidden = struct end;
    15 structure Hidden = struct end;
    17 
    16 
    18 (*basic tools*)
    17 (*basic tools*)
    35 use "unify.ML";
    34 use "unify.ML";
    36 use "net.ML";
    35 use "net.ML";
    37 use "logic.ML";
    36 use "logic.ML";
    38 use "theory.ML";
    37 use "theory.ML";
    39 use "theory_data.ML";
    38 use "theory_data.ML";
       
    39 use "object_logic.ML";
    40 use "thm.ML";
    40 use "thm.ML";
    41 use "display.ML";
    41 use "display.ML";
    42 use "attribute.ML";
    42 use "attribute.ML";
    43 use "pure_thy.ML";
    43 use "pure_thy.ML";
    44 use "deriv.ML";
    44 use "deriv.ML";
    50 use "goals.ML";
    50 use "goals.ML";
    51 use "axclass.ML";
    51 use "axclass.ML";
    52 
    52 
    53 (*theory parser and loader*)
    53 (*theory parser and loader*)
    54 cd "Thy";
    54 cd "Thy";
       
    55 use "ROOT.ML";
       
    56 cd "..";
       
    57 
       
    58 (*the Isar subsystem*)
       
    59 cd "Isar";
    55 use "ROOT.ML";
    60 use "ROOT.ML";
    56 cd "..";
    61 cd "..";
    57 
    62 
    58 use "pure.ML";
    63 use "pure.ML";
    59 
    64 
    73 end;
    78 end;
    74 
    79 
    75 open Use;
    80 open Use;
    76 
    81 
    77 print_depth 8;
    82 print_depth 8;
       
    83 (*ml_prompts "ML> " "ML# ";*)