equal
deleted
inserted
replaced
83 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
83 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" |
84 | "bv_cvs CvsNil = []" |
84 | "bv_cvs CvsNil = []" |
85 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
85 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
86 |
86 |
87 (* generated theorems *) |
87 (* generated theorems *) |
|
88 |
|
89 thm core_haskell.perm_bn_alpha |
|
90 thm core_haskell.perm_bn_simps |
|
91 thm core_haskell.bn_finite |
88 |
92 |
89 thm core_haskell.distinct |
93 thm core_haskell.distinct |
90 thm core_haskell.induct |
94 thm core_haskell.induct |
91 thm core_haskell.exhaust |
95 thm core_haskell.exhaust |
92 thm core_haskell.fv_defs |
96 thm core_haskell.fv_defs |