src/Pure/ROOT.ML
changeset 5684 9a3acc4c7c2e
parent 5607 5db9e2343ade
child 5834 c6fea8488ce7
equal deleted inserted replaced
5683:e62518aacc5b 5684:9a3acc4c7c2e
    10 val version = "Isabelle repository";
    10 val version = "Isabelle repository";
    11 
    11 
    12 print_depth 1;
    12 print_depth 1;
    13 ml_prompts "> " "# ";
    13 ml_prompts "> " "# ";
    14 
    14 
       
    15 (*fake hiding of private structures*)
       
    16 structure Hidden = struct end;
    15 
    17 
    16 (*basic tools*)
    18 (*basic tools*)
    17 use "library.ML";
    19 use "library.ML";
    18 cd "General"; use "ROOT.ML"; cd "..";
    20 cd "General"; use "ROOT.ML"; cd "..";
    19 use "term.ML";
    21 use "term.ML";