| changeset 520 | cc1f240d8cf4 |
| parent 518 | 14f68c1f4d12 |
| child 521 | fdfeef0399f7 |
| 518:14f68c1f4d12 | 520:cc1f240d8cf4 |
|---|---|
803 val thy = ProofContext.theory_of context; |
803 val thy = ProofContext.theory_of context; |
804 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d]; |
804 val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d]; |
805 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
805 val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y]; |
806 val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y]; |
806 val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y]; |
807 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP} |
807 val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP} |
808 (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*) |
808 val _ = tracing ("instantiated rule" ^ Syntax.string_of_term @{context} (prop_of thm)) |
809 in |
809 in |
810 rtac thm 1 |
810 rtac thm 1 |
811 end |
811 end |
812 end |
812 end |
813 | _ => no_tac) |
813 | _ => no_tac) |