src/Pure/ROOT.ML
changeset 2 c67f44be880f
parent 0 a5a9c433f639
child 19 929ad32d63fc
equal deleted inserted replaced
1:c6a6e3db5353 2:c67f44be880f
    23 use "symtab.ML";
    23 use "symtab.ML";
    24 
    24 
    25 (*Used for building the parser generator*)
    25 (*Used for building the parser generator*)
    26 structure Symtab = SymtabFun();
    26 structure Symtab = SymtabFun();
    27 cd "Syntax";
    27 cd "Syntax";
    28 use "ROOT.ML";
       
    29 cd "..";
       
    30 
       
    31 (* Theory parser *)
       
    32 cd "Thy";
       
    33 use "ROOT.ML";
    28 use "ROOT.ML";
    34 cd "..";
    29 cd "..";
    35 
    30 
    36 print_depth 1;
    31 print_depth 1;
    37 use "type.ML";
    32 use "type.ML";
    67 structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    62 structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    68 			   and Tactic=Tactic and Pattern=Pattern);
    63 			   and Tactic=Tactic and Pattern=Pattern);
    69 open Basic_Syntax Thm Drule Tactical Tactic Goals;
    64 open Basic_Syntax Thm Drule Tactical Tactic Goals;
    70 
    65 
    71 structure Pure = struct val thy = pure_thy end;
    66 structure Pure = struct val thy = pure_thy end;
       
    67 
       
    68 (* Theory parser *)
       
    69 cd "Thy";
       
    70 use "ROOT.ML";
       
    71 cd "..";
       
    72