equal
deleted
inserted
replaced
496 by (simp_tac (simpset() addsimps [subst_comp_scheme_list]) 1); |
496 by (simp_tac (simpset() addsimps [subst_comp_scheme_list]) 1); |
497 by (simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym]) 1); |
497 by (simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym]) 1); |
498 by (res_inst_tac [("A2","($ Sa ($ S A))")] |
498 by (res_inst_tac [("A2","($ Sa ($ S A))")] |
499 ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1); |
499 ((subst_comp_scheme_list RS sym) RSN (2,trans)) 1); |
500 by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1); |
500 by ( asm_full_simp_tac (simpset() addsimps [o_def,eq_sym_conv]) 1); |
501 by(dres_inst_tac [("s","Some ?X")] sym 1); |
501 by (dres_inst_tac [("s","Some ?X")] sym 1); |
502 by (rtac eq_free_eq_subst_scheme_list 1); |
502 by (rtac eq_free_eq_subst_scheme_list 1); |
503 by ( safe_tac HOL_cs ); |
503 by ( safe_tac HOL_cs ); |
504 by (subgoal_tac "ma ~= na" 1); |
504 by (subgoal_tac "ma ~= na" 1); |
505 by ((forward_tac [new_tv_W] 2) THEN (atac 2)); |
505 by ((forward_tac [new_tv_W] 2) THEN (atac 2)); |
506 by (etac conjE 2); |
506 by (etac conjE 2); |