--- 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];
--- a/Nat.ML Thu Nov 25 10:04:02 1993 +0100
+++ b/Nat.ML Mon Nov 29 18:35:02 1993 +0100
@@ -349,7 +349,7 @@
Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
-val nat_ss = pair_ss addsimps nat_simps;
+val nat_ss = sum_ss addsimps nat_simps;
(*Prevents simplification of f and g: much faster*)
val nat_case_weak_cong = prove_goal Nat.thy
--- a/nat.ML Thu Nov 25 10:04:02 1993 +0100
+++ b/nat.ML Mon Nov 29 18:35:02 1993 +0100
@@ -349,7 +349,7 @@
Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
-val nat_ss = pair_ss addsimps nat_simps;
+val nat_ss = sum_ss addsimps nat_simps;
(*Prevents simplification of f and g: much faster*)
val nat_case_weak_cong = prove_goal Nat.thy