equal
deleted
inserted
replaced
185 tac ctxt, |
185 tac ctxt, |
186 tac ctxt]; |
186 tac ctxt]; |
187 fun prove_one_point_all_tac ctxt = |
187 fun prove_one_point_all_tac ctxt = |
188 EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI}, |
188 EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI}, |
189 resolve_tac ctxt [@{thm equal_allI}], |
189 resolve_tac ctxt [@{thm equal_allI}], |
|
190 Object_Logic.full_atomize_tac ctxt, |
190 resolve_tac ctxt [@{thm equal_intr_rule}], |
191 resolve_tac ctxt [@{thm equal_intr_rule}], |
191 Object_Logic.atomize_prems_tac ctxt, |
|
192 tac ctxt, |
192 tac ctxt, |
193 Object_Logic.atomize_prems_tac ctxt, |
|
194 tac ctxt]; |
193 tac ctxt]; |
195 end |
194 end |
196 |
195 |
197 fun prove_conv ctxt tu tac = |
196 fun prove_conv ctxt tu tac = |
198 let |
197 let |