src/Pure/ROOT.ML
changeset 4949 c73f72daee64
parent 4781 6b55d02437ad
child 4962 e9217cb15b42
equal deleted inserted replaced
4948:c53aa26ccfd2 4949:c73f72daee64
    10 val banner = "Pure Isabelle";
    10 val banner = "Pure Isabelle";
    11 val version = "Isabelle98: January 1998";
    11 val version = "Isabelle98: January 1998";
    12 
    12 
    13 print_depth 1;
    13 print_depth 1;
    14 
    14 
       
    15 
       
    16 (*basic utils*)
    15 use "library.ML";
    17 use "library.ML";
    16 use "table.ML";
    18 use "table.ML";
    17 use "seq.ML";
    19 use "seq.ML";
    18 use "name_space.ML";
    20 use "name_space.ML";
    19 use "term.ML";
    21 use "term.ML";
    20 
    22 
    21 (*Syntax module*)
    23 (*inner syntax module*)
    22 cd "Syntax";
    24 cd "Syntax";
    23 use "ROOT.ML";
    25 use "ROOT.ML";
    24 cd "..";
    26 cd "..";
    25 
    27 
    26 (*Main system*)
    28 (*main system*)
    27 use "sorts.ML";
    29 use "sorts.ML";
    28 use "type_infer.ML";
    30 use "type_infer.ML";
    29 use "type.ML";
    31 use "type.ML";
    30 use "sign.ML";
    32 use "sign.ML";
    31 use "envir.ML";
    33 use "envir.ML";
    44 use "search.ML";
    46 use "search.ML";
    45 use "tactic.ML";
    47 use "tactic.ML";
    46 use "goals.ML";
    48 use "goals.ML";
    47 use "axclass.ML";
    49 use "axclass.ML";
    48 
    50 
    49 (*Theory parser and loader*)
    51 (*theory parser and loader*)
    50 val global_names = ref false;		(* FIXME tmp *)
    52 val global_names = ref false;		(* FIXME tmp *)
    51 cd "Thy";
    53 cd "Thy";
    52 use "ROOT.ML";
    54 use "ROOT.ML";
    53 cd "..";
    55 cd "..";
    54 
    56