equal
deleted
inserted
replaced
6 |
6 |
7 infix 8 % %% %>; |
7 infix 8 % %% %>; |
8 |
8 |
9 signature BASIC_PROOFTERM = |
9 signature BASIC_PROOFTERM = |
10 sig |
10 sig |
11 val proofs: int Unsynchronized.ref |
|
12 |
|
13 type thm_node |
11 type thm_node |
14 datatype proof = |
12 datatype proof = |
15 MinProof |
13 MinProof |
16 | PBound of int |
14 | PBound of int |
17 | Abst of string * typ option * proof |
15 | Abst of string * typ option * proof |
26 | PThm of serial * ((string * term * typ list option) * proof_body future) |
24 | PThm of serial * ((string * term * typ list option) * proof_body future) |
27 and proof_body = PBody of |
25 and proof_body = PBody of |
28 {oracles: (string * term) Ord_List.T, |
26 {oracles: (string * term) Ord_List.T, |
29 thms: (serial * thm_node) Ord_List.T, |
27 thms: (serial * thm_node) Ord_List.T, |
30 proof: proof} |
28 proof: proof} |
31 |
|
32 val %> : proof * term -> proof |
29 val %> : proof * term -> proof |
33 end; |
30 end; |
34 |
31 |
35 signature PROOFTERM = |
32 signature PROOFTERM = |
36 sig |
33 sig |
37 include BASIC_PROOFTERM |
34 include BASIC_PROOFTERM |
38 |
35 val proofs: int Unsynchronized.ref |
39 type pthm = serial * thm_node |
36 type pthm = serial * thm_node |
40 type oracle = string * term |
37 type oracle = string * term |
41 val proof_of: proof_body -> proof |
38 val proof_of: proof_body -> proof |
42 val thm_node_name: thm_node -> string |
39 val thm_node_name: thm_node -> string |
43 val thm_node_prop: thm_node -> term |
40 val thm_node_prop: thm_node -> term |