equal
deleted
inserted
replaced
257 "(t::typ) mem ts --> free_tv t <= free_tv ts"; |
257 "(t::typ) mem ts --> free_tv t <= free_tv ts"; |
258 by (list.induct_tac "ts" 1); |
258 by (list.induct_tac "ts" 1); |
259 (* case [] *) |
259 (* case [] *) |
260 by (Simp_tac 1); |
260 by (Simp_tac 1); |
261 (* case x#xl *) |
261 (* case x#xl *) |
262 by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 1); |
262 by (fast_tac (set_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1); |
263 qed_spec_mp "ftv_mem_sub_ftv_list"; |
263 qed_spec_mp "ftv_mem_sub_ftv_list"; |
264 Addsimps [ftv_mem_sub_ftv_list]; |
264 Addsimps [ftv_mem_sub_ftv_list]; |
265 |
265 |
266 |
266 |
267 (* if two substitutions yield the same result if applied to a type |
267 (* if two substitutions yield the same result if applied to a type |