equal
deleted
inserted
replaced
6 |
6 |
7 atom_decl var |
7 atom_decl var |
8 atom_decl cvar |
8 atom_decl cvar |
9 atom_decl tvar |
9 atom_decl tvar |
10 |
10 |
11 declare [[STEPS = 16]] |
11 declare [[STEPS = 17]] |
12 |
12 |
13 nominal_datatype tkind = |
13 nominal_datatype tkind = |
14 KStar |
14 KStar |
15 | KFun "tkind" "tkind" |
15 | KFun "tkind" "tkind" |
16 and ckind = |
16 and ckind = |
83 | "bv_tvs TvsNil = []" |
83 | "bv_tvs TvsNil = []" |
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 thm alpha_sym_thms |
|
89 thm funs_rsp |
|
90 thm distinct |
88 |
91 |
89 term TvsNil |
92 term TvsNil |
90 |
93 |
91 |
94 |
92 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
95 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |