equal
deleted
inserted
replaced
137 val nth_drop = thm "nth_drop"; |
137 val nth_drop = thm "nth_drop"; |
138 val nth_equalityI = thm "nth_equalityI"; |
138 val nth_equalityI = thm "nth_equalityI"; |
139 val nth_list_update = thm "nth_list_update"; |
139 val nth_list_update = thm "nth_list_update"; |
140 val nth_list_update_eq = thm "nth_list_update_eq"; |
140 val nth_list_update_eq = thm "nth_list_update_eq"; |
141 val nth_list_update_neq = thm "nth_list_update_neq"; |
141 val nth_list_update_neq = thm "nth_list_update_neq"; |
142 val nth_map = thm "nth_map"; |
|
143 val nth_map_upt = thm "nth_map_upt"; |
142 val nth_map_upt = thm "nth_map_upt"; |
144 val nth_mem = thm "nth_mem"; |
143 val nth_mem = thm "nth_mem"; |
145 val nth_replicate = thm "nth_replicate"; |
144 val nth_replicate = thm "nth_replicate"; |
146 val nth_take = thm "nth_take"; |
145 val nth_take = thm "nth_take"; |
147 val nth_take_lemma = thm "nth_take_lemma"; |
146 val nth_take_lemma = thm "nth_take_lemma"; |