27 |
27 |
28 |
28 |
29 |
29 |
30 (* A record containing all the relevant symbols and types needed during the proof. |
30 (* A record containing all the relevant symbols and types needed during the proof. |
31 This is set up at the beginning and does not change. *) |
31 This is set up at the beginning and does not change. *) |
32 type naming_context = |
32 datatype naming_context = |
33 { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ, |
33 Names of { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ, |
34 G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, |
34 G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, |
35 D: term, Pbool:term, |
35 D: term, Pbool:term, |
36 glrs: (term list * term list * term * term) list, |
36 glrs: (term list * term list * term * term) list, |
37 glrs': (term list * term list * term * term) list, |
37 glrs': (term list * term list * term * term) list, |
38 f_def: thm, |
38 f_def: thm, |
39 used: string list, |
39 used: string list, |
40 trees: ctx_tree list |
40 trees: ctx_tree list |
41 } |
41 } |
42 |
42 |
43 |
43 |
44 type rec_call_info = |
44 datatype rec_call_info = |
45 {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} |
45 RCInfo of {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} |
46 |
46 |
47 type clause_info = |
47 datatype clause_info = |
|
48 ClauseInfo of |
48 { |
49 { |
49 no: int, |
50 no: int, |
50 |
51 |
51 qs: term list, |
52 qs: term list, |
52 gs: term list, |
53 gs: term list, |