equal
deleted
inserted
replaced
11 val version = "Isabelle-94 revision 8: May 1997"; |
11 val version = "Isabelle-94 revision 8: May 1997"; |
12 |
12 |
13 print_depth 1; |
13 print_depth 1; |
14 |
14 |
15 use "library.ML"; |
15 use "library.ML"; |
|
16 use "seq.ML"; |
16 use "symtab.ML"; |
17 use "symtab.ML"; |
17 use "name_space.ML"; |
18 use "name_space.ML"; |
18 use "term.ML"; |
19 use "term.ML"; |
19 |
20 |
20 (*Syntax module*) |
21 (*Syntax module*) |
25 (*Core system*) |
26 (*Core system*) |
26 use "sorts.ML"; |
27 use "sorts.ML"; |
27 use "type_infer.ML"; |
28 use "type_infer.ML"; |
28 use "type.ML"; |
29 use "type.ML"; |
29 use "sign.ML"; |
30 use "sign.ML"; |
30 use "seq.ML"; |
|
31 use "envir.ML"; |
31 use "envir.ML"; |
32 use "pattern.ML"; |
32 use "pattern.ML"; |
33 use "unify.ML"; |
33 use "unify.ML"; |
34 use "net.ML"; |
34 use "net.ML"; |
35 use "logic.ML"; |
35 use "logic.ML"; |