equal
deleted
inserted
replaced
8 signature SLEDGEHAMMER_FACT = |
8 signature SLEDGEHAMMER_FACT = |
9 sig |
9 sig |
10 type status = ATP_Problem_Generate.status |
10 type status = ATP_Problem_Generate.status |
11 type stature = ATP_Problem_Generate.stature |
11 type stature = ATP_Problem_Generate.stature |
12 |
12 |
13 type raw_fact = ((unit -> string) * stature) * thm |
13 type raw_fact = ((unit -> string) * stature) * thm (* TODO: rename to lazy_fact *) |
14 type fact = (string * stature) * thm |
14 type fact = (string * stature) * thm |
15 |
15 |
16 type fact_override = |
16 type fact_override = |
17 {add : (Facts.ref * Token.src list) list, |
17 {add : (Facts.ref * Token.src list) list, |
18 del : (Facts.ref * Token.src list) list, |
18 del : (Facts.ref * Token.src list) list, |