equal
deleted
inserted
replaced
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
84 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
85 | "bv_cvs CvsNil = []" |
85 | "bv_cvs CvsNil = []" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
86 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
87 |
87 |
88 (* can lift *) |
88 (* can lift *) |
|
89 |
89 thm distinct |
90 thm distinct |
90 thm fv_defs |
91 thm fv_defs |
91 thm alpha_bn_imps alpha_equivp |
92 thm alpha_bn_imps alpha_equivp |
92 |
93 |
93 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts |
94 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts |
94 thm perm_simps |
95 thm perm_simps |
95 thm perm_laws |
96 thm perm_laws |
96 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98) |
97 thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98) |
97 |
98 |
98 (* cannot lift yet *) |
|
99 thm eq_iff |
99 thm eq_iff |
100 thm eq_iff_simps |
100 thm eq_iff_simps |
101 |
101 |
102 ML {* |
102 ML {* |
103 val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co}, |
103 val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co}, |