equal
deleted
inserted
replaced
178 by (expr.induct_tac "e" 1); |
178 by (expr.induct_tac "e" 1); |
179 (* case Var n *) |
179 (* case Var n *) |
180 by (simp_tac (simpset() addsimps |
180 by (simp_tac (simpset() addsimps |
181 [free_tv_subst] addsplits [split_option_bind,expand_if]) 1); |
181 [free_tv_subst] addsplits [split_option_bind,expand_if]) 1); |
182 by (strip_tac 1); |
182 by (strip_tac 1); |
183 by (case_tac "v : free_tv (nth nat A)" 1); |
183 by (case_tac "v : free_tv (A!nat)" 1); |
184 by (Asm_full_simp_tac 1); |
184 by (Asm_full_simp_tac 1); |
185 by (dtac free_tv_bound_typ_inst1 1); |
185 by (dtac free_tv_bound_typ_inst1 1); |
186 by (simp_tac (simpset() addsimps [o_def]) 1); |
186 by (simp_tac (simpset() addsimps [o_def]) 1); |
187 by (etac exE 1); |
187 by (etac exE 1); |
188 by (rotate_tac 3 1); |
188 by (rotate_tac 3 1); |