equal
deleted
inserted
replaced
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; |