equal
deleted
inserted
replaced
93 fun prove thy r asms = |
93 fun prove thy r asms = |
94 let |
94 let |
95 fun inst thm = |
95 fun inst thm = |
96 let val SOME (_, _, r', _) = decomp (concl_of thm) |
96 let val SOME (_, _, r', _) = decomp (concl_of thm) |
97 in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end; |
97 in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end; |
98 fun pr (Asm i) = List.nth (asms, i) |
98 fun pr (Asm i) = nth asms i |
99 | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm |
99 | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm; |
100 in pr end; |
100 in pr end; |
101 |
101 |
102 |
102 |
103 (* Internal datatype for inequalities *) |
103 (* Internal datatype for inequalities *) |
104 datatype rel |
104 datatype rel |