equal
deleted
inserted
replaced
1007 apply (assumption) |
1007 apply (assumption) |
1008 apply (metis) |
1008 apply (metis) |
1009 done |
1009 done |
1010 |
1010 |
1011 ML {* |
1011 ML {* |
1012 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, context, ...} => |
1012 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => |
1013 let |
1013 let |
1014 val pat = Drule.strip_imp_concl (cprop_of thm) |
1014 val pat = Drule.strip_imp_concl (cprop_of thm) |
1015 val insts = Thm.match (pat, concl) |
1015 val insts = Thm.match (pat, concl) |
1016 in |
1016 in |
1017 rtac (Drule.instantiate insts thm) 1 |
1017 rtac (Drule.instantiate insts thm) 1 |