equal
deleted
inserted
replaced
72 \ A) = \ |
72 \ A) = \ |
73 \ ($ ((%x. if x : free_tv A Un free_tv t then S x \ |
73 \ ($ ((%x. if x : free_tv A Un free_tv t then S x \ |
74 \ else TVar x) o \ |
74 \ else TVar x) o \ |
75 \ (%x. if x : free_tv A \ |
75 \ (%x. if x : free_tv A \ |
76 \ then x else n + x)) A)"; |
76 \ then x else n + x)) A)"; |
77 by (rtac (S_o_alpha_type_scheme_list RS ssubst) 1); |
77 by (stac S_o_alpha_type_scheme_list 1); |
78 by (rtac (alpha_A RS ssubst) 1); |
78 by (stac alpha_A 1); |
79 by (rtac refl 1); |
79 by (rtac refl 1); |
80 qed "S'_A_eq_S'_alpha_A"; |
80 qed "S'_A_eq_S'_alpha_A"; |
81 |
81 |
82 goalw thy [free_tv_subst,dom_def] |
82 goalw thy [free_tv_subst,dom_def] |
83 "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ |
83 "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \ |