
diff -r 90ada01470cb -r eb1e5c4f70cd src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Dec 19 09:33:11 2020 +0000
+++ b/src/HOL/Library/Word.thy	Sat Dec 19 17:49:14 2020 +0000
@@ -3227,7 +3227,8 @@
 \<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
 ML \<open>
 val unat_arith_simpset =
-  @{context}
+  @{context} (* TODO: completely explicitly determined simpset *)
+  |> fold Simplifier.del_simp @{thms unsigned_of_nat unsigned_of_int}
   |> fold Simplifier.add_simp @{thms unat_arith_simps}
   |> fold Splitter.add_split @{thms if_split_asm}
   |> fold Simplifier.add_cong @{thms power_False_cong}




