fix(proofs): finish Isabelle base corpus repair (polymorphic nat/list lemmas)

proofs/isabelle/EchidnaList.thy

@@ -248,7 +248,7 @@ text \<open>
 
 lemma map_rev:
   "map f (rev xs) = rev (map f xs)"
-  by simp
+  by (simp add: rev_map)
 
 section \<open>Filter Function\<close>
 

proofs/isabelle/EchidnaNat.thy

@@ -47,15 +47,15 @@ text \<open>
 \<close>
 
 lemma add_assoc:
-  "(m + n) + p = m + (n + p)"
+  "((m::nat) + n) + p = m + (n + p)"
   by simp
 
 text \<open>
   Explicit inductive proof of right zero for addition.
 \<close>
 
 lemma add_zero_right_inductive:
-  shows "n + 0 = n"
+  shows "(n::nat) + 0 = n"
 proof (induction n)
   case 0
   show ?case by simp
@@ -71,31 +71,31 @@ text \<open>
 \<close>
 
 lemma mult_zero_left:
-  "0 * n = 0"
+  "(0::nat) * n = 0"
   by simp
 
 lemma mult_zero_right:
-  "n * 0 = 0"
+  "(n::nat) * 0 = 0"
   by simp
 
 text \<open>
   Multiplication with one (identity).
 \<close>
 
 lemma mult_one_left:
-  "1 * n = n"
+  "(1::nat) * n = n"
   by simp
 
 lemma mult_one_right:
-  "n * 1 = n"
+  "(n::nat) * 1 = n"
   by simp
 
 text \<open>
   Multiplication is commutative.
 \<close>
 
 lemma mult_comm:
-  "m * n = n * m"
+  "(m::nat) * n = n * m"
   by simp
 
 text \<open>