Added rev_append and rev_rev_ident to list_ss.
authornipkow
Thu, 27 Jul 1995 18:28:14 +0200
changeset 1202 968cd786a748
parent 1201 de2fc8cf9b6a
child 1203 a39bec971684
Added rev_append and rev_rev_ident to list_ss.
src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Jul 27 13:13:32 1995 +0200
+++ b/src/HOL/List.ML	Thu Jul 27 18:28:14 1995 +0200
@@ -183,6 +183,7 @@
 val list_ss = list_ss addsimps
   [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
    mem_append, mem_filter,
+   rev_append, rev_rev_ident,
    map_ident, map_append, map_compose,
    flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];