| changeset 2399 | 107c06267f33 |
| parent 2398 | 1e6160690546 |
| child 2400 | c6d30d5f5ba1 |
| 2398:1e6160690546 | 2399:107c06267f33 |
|---|---|
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 |
88 |
89 thm funs_rsp |
|
90 thm distinct |
89 thm distinct |
91 |
90 |
92 term TvsNil |
91 term TvsNil |
93 |
92 |
94 |
93 |