| changeset 523 | 1a4eb39ba834 |
| parent 522 | 6b77cfd508e9 |
| parent 521 | fdfeef0399f7 |
| child 524 | c7c6ba5ac043 |
| child 525 | 3f657c4fbefa |
| 522:6b77cfd508e9 | 523:1a4eb39ba834 |
|---|---|
792 val thy = ProofContext.theory_of context; |
792 val thy = ProofContext.theory_of context; |
793 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d]; |
793 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d]; |
794 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
794 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
795 val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y]; |
795 val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y]; |
796 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP} |
796 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP} |
797 (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*) |
797 val _ = tracing ("instantiated rule" ^ Syntax.string_of_term @{context} (prop_of thm)) |
798 in |
798 in |
799 rtac thm 1 |
799 rtac thm 1 |
800 end |
800 end |
801 end |
801 end |
802 | _ => no_tac) |
802 | _ => no_tac) |