--- 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}