diff -r da15d528fb19 -r f4f9946ad741 List.ML --- a/List.ML Thu Nov 25 10:04:02 1993 +0100 +++ b/List.ML Mon Nov 29 18:35:02 1993 +0100 @@ -374,3 +374,12 @@ by(ALLGOALS(asm_simp_tac(map_ss addsimps [Rep_map_type,List_Sexp RS subsetD]))); val Abs_Rep_map = result(); + +val list_ss = arith_ss addsimps + [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, + list_rec_Nil, list_rec_Cons, + null_Nil, null_Cons, hd_Cons, tl_Cons, + list_case_Nil, list_case_Cons, + append_Nil, append_Cons, append_assoc, + map_Nil, map_Cons, map_ident, + list_all_Nil, list_all_Cons];