equal
deleted
inserted
replaced
791 |> cterm_of thy |
791 |> cterm_of thy |
792 in |
792 in |
793 Goal.init goal |
793 Goal.init goal |
794 |> (SINGLE (resolve_tac [accI] 1)) |> the |
794 |> (SINGLE (resolve_tac [accI] 1)) |> the |
795 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
795 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
796 |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the |
796 |> (SINGLE (auto_tac ctxt)) |> the |
797 |> Goal.conclude |
797 |> Goal.conclude |
798 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
798 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
799 end |
799 end |
800 |
800 |
801 |
801 |