# HG changeset patch
# User nipkow
# Date 806862494 -7200
# Node ID 968cd786a748328ecdc00accde496fb27ab41991
# Parent  de2fc8cf9b6aef9fcfc6b5e3f0902de7550eed83
Added rev_append and rev_rev_ident to list_ss.

diff -r de2fc8cf9b6a -r 968cd786a748 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];