equal
deleted
inserted
replaced
640 |
640 |
641 |
641 |
642 (* meta-level conjunction *) |
642 (* meta-level conjunction *) |
643 |
643 |
644 val conj_tac = SUBGOAL (fn (goal, i) => |
644 val conj_tac = SUBGOAL (fn (goal, i) => |
645 if can Logic.dest_conjunction goal then |
645 if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i |
646 (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st) |
|
647 else no_tac); |
646 else no_tac); |
648 |
647 |
649 val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac; |
648 val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac; |
650 |
649 |
651 val precise_conjunction_tac = |
650 val precise_conjunction_tac = |