equal
deleted
inserted
replaced
511 by (eres_inst_tac [("x","t2")] allE 1); |
511 by (eres_inst_tac [("x","t2")] allE 1); |
512 by (eres_inst_tac [("x","m")] allE 1); |
512 by (eres_inst_tac [("x","m")] allE 1); |
513 by (rotate_tac ~3 1); |
513 by (rotate_tac ~3 1); |
514 by (Asm_full_simp_tac 1); |
514 by (Asm_full_simp_tac 1); |
515 by (safe_tac HOL_cs); |
515 by (safe_tac HOL_cs); |
|
516 by (contr_tac 1); |
516 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS |
517 by (fast_tac (HOL_cs addIs [sym RS W_var_geD,new_tv_W RS |
517 conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1); |
518 conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1); |
518 |
519 (** LEVEL 35 **) |
519 by (subgoal_tac |
520 by (subgoal_tac |
520 "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
521 "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
521 \ else Ra x)) ($ Sa t) = \ |
522 \ else Ra x)) ($ Sa t) = \ |
522 \ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
523 \ $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \ |
523 \ else Ra x)) (ta -> (TVar ma))" 1); |
524 \ else Ra x)) (ta -> (TVar ma))" 1); |