ETCSprover/master.ML at master · u5943321/ETCSprover · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
use "term.sig";
use "term.sml";
open term;


use "form.sig";
use "form.sml";
open form;

use "logic.sig";
use "logic.sml";
open logic;

use "pp.sig";
use "pp.sml";
open pp;

use "token.sig";
use "token.sml";
open token;

use "pterm_dtype.sml";
open pterm_dtype;


use "parser.sig";
use "parser.sml";
open parser;

use "drule.sig";
use "drule.sml";
open drule;

use "infixes.sml";
use "abbrev.sig";
use "abbrev.sml";
open abbrev;


use "conv.sig";
use "conv.sml";
open conv;

use "tactic.sig";
use "tactic.sml";
open tactic;


use "goalstack.sig";
use "goalstack.sml";
open goalstack;

use "iffLR.sml";
use "irule_canon.sml";
use "q.sml";
use "proofmanager.sml";