equal
deleted
inserted
replaced
543 in |
543 in |
544 Subgoal.FOCUS (fn {prems, concl, ...} => |
544 Subgoal.FOCUS (fn {prems, concl, ...} => |
545 let |
545 let |
546 val SOME (_, _, rel', _) = decomp (term_of concl); |
546 val SOME (_, _, rel', _) = decomp (term_of concl); |
547 val thms = map (prove thy rel' prems) prfs |
547 val thms = map (prove thy rel' prems) prfs |
548 in rtac (prove thy rel' thms prf) 1 end) ctxt n st |
548 in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st |
549 end |
549 end |
550 handle Cannot => Seq.empty); |
550 handle Cannot => Seq.empty); |
551 |
551 |
552 |
552 |
553 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st => |
553 fun rtrancl_tac ctxt = SUBGOAL (fn (A, n) => fn st => |
562 in |
562 in |
563 Subgoal.FOCUS (fn {prems, concl, ...} => |
563 Subgoal.FOCUS (fn {prems, concl, ...} => |
564 let |
564 let |
565 val SOME (_, _, rel', _) = decomp (term_of concl); |
565 val SOME (_, _, rel', _) = decomp (term_of concl); |
566 val thms = map (prove thy rel' prems) prfs |
566 val thms = map (prove thy rel' prems) prfs |
567 in rtac (prove thy rel' thms prf) 1 end) ctxt n st |
567 in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st |
568 end |
568 end |
569 handle Cannot => Seq.empty | General.Subscript => Seq.empty); |
569 handle Cannot => Seq.empty | General.Subscript => Seq.empty); |
570 |
570 |
571 end; |
571 end; |