equal
deleted
inserted
replaced
22 |
22 |
23 (* ------------------------------------------------------------------------- *) |
23 (* ------------------------------------------------------------------------- *) |
24 (* Reconstructing single inferences. *) |
24 (* Reconstructing single inferences. *) |
25 (* ------------------------------------------------------------------------- *) |
25 (* ------------------------------------------------------------------------- *) |
26 |
26 |
|
27 val inferenceType : inference -> Thm.inferenceType |
|
28 |
|
29 val parents : inference -> Thm.thm list |
|
30 |
27 val inferenceToThm : inference -> Thm.thm |
31 val inferenceToThm : inference -> Thm.thm |
28 |
32 |
29 val thmToInference : Thm.thm -> inference |
33 val thmToInference : Thm.thm -> inference |
30 |
34 |
31 (* ------------------------------------------------------------------------- *) |
35 (* ------------------------------------------------------------------------- *) |