src/Pure/Isar/ROOT.ML
changeset 12936 84eb6c75cfe3
parent 12882 e20f14f7ff35
child 13369 dc5d2a0685eb
equal deleted inserted replaced
12935:d697091d1591 12936:84eb6c75cfe3
    35 (*toplevel environment*)
    35 (*toplevel environment*)
    36 use "toplevel.ML";
    36 use "toplevel.ML";
    37 use "session.ML";
    37 use "session.ML";
    38 use "isar_output.ML";
    38 use "isar_output.ML";
    39 
    39 
       
    40 (*theory syntax*)
       
    41 use "thy_header.ML";
       
    42 use "outer_syntax.ML";
       
    43 
    40 (*theory and proof operations*)
    44 (*theory and proof operations*)
    41 use "isar_thy.ML";
    45 use "isar_thy.ML";
    42 use "isar_cmd.ML";
    46 use "isar_cmd.ML";
    43 
       
    44 (*theory syntax*)
       
    45 use "thy_header.ML";
       
    46 use "outer_syntax.ML";
       
    47 use "isar_syn.ML";
    47 use "isar_syn.ML";
    48 
    48 
    49 (*main ML interfaces*)
    49 (*main ML interfaces*)
    50 use "isar.ML";
    50 use "isar.ML";
    51 
    51 
    67   structure OuterLex = OuterLex;
    67   structure OuterLex = OuterLex;
    68   structure Antiquote = Antiquote;
    68   structure Antiquote = Antiquote;
    69   structure OuterParse = OuterParse;
    69   structure OuterParse = OuterParse;
    70   structure Toplevel = Toplevel;
    70   structure Toplevel = Toplevel;
    71   structure Session = Session;
    71   structure Session = Session;
    72   structure IsarThy = IsarThy;
       
    73   structure IsarOutput = IsarOutput;
    72   structure IsarOutput = IsarOutput;
    74   structure IsarCmd = IsarCmd;
       
    75   structure ThyHeader = ThyHeader;
    73   structure ThyHeader = ThyHeader;
    76   structure OuterSyntax = OuterSyntax;
    74   structure OuterSyntax = OuterSyntax;
       
    75   structure IsarThy = IsarThy;
       
    76   structure IsarCmd = IsarCmd;
    77   structure IsarSyn = IsarSyn;
    77   structure IsarSyn = IsarSyn;
    78   structure Isar = Isar;
    78   structure Isar = Isar;
    79 end;
    79 end;