equal
deleted
inserted
replaced
546 (* instantiates exI with the permutation p + q *) |
546 (* instantiates exI with the permutation p + q *) |
547 val perm_inst_tac = |
547 val perm_inst_tac = |
548 Subgoal.FOCUS (fn {params, ...} => |
548 Subgoal.FOCUS (fn {params, ...} => |
549 let |
549 let |
550 val (p, q) = pairself snd (last2 params) |
550 val (p, q) = pairself snd (last2 params) |
551 val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q] |
551 val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] |
552 val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} |
552 val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} |
553 in |
553 in |
554 HEADGOAL (rtac exi_inst) |
554 HEADGOAL (rtac exi_inst) |
555 end) |
555 end) |
556 |
556 |