src/HOL/MiniML/W.ML
changeset 2779 9c42ae57b5f4
parent 2749 2f477a0e690d
child 2793 b30c41754c86
equal deleted inserted replaced
2778:40219658ce64 2779:9c42ae57b5f4
   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);