equal
deleted
inserted
replaced
84 assumptions. *) |
84 assumptions. *) |
85 exception Contr of proof; |
85 exception Contr of proof; |
86 (* Internal exception, raised if contradiction ( x < x ) was derived *) |
86 (* Internal exception, raised if contradiction ( x < x ) was derived *) |
87 |
87 |
88 fun prove asms = |
88 fun prove asms = |
89 let fun pr (Asm i) = List.nth (asms, i) |
89 let |
90 | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm |
90 fun pr (Asm i) = nth asms i |
|
91 | pr (Thm (prfs, thm)) = map pr prfs MRS thm; |
91 in pr end; |
92 in pr end; |
92 |
93 |
93 (* Internal datatype for inequalities *) |
94 (* Internal datatype for inequalities *) |
94 datatype less |
95 datatype less |
95 = Less of term * term * proof |
96 = Less of term * term * proof |