# HG changeset patch
# User haftmann
# Date 1608400154 0
# Node ID eb1e5c4f70cd6d890f9f5ecd9a8e8bf2f083a4e5
# Parent  90ada01470cbd6ef6e2ca160c541b094704c230b
more precise simpset for method unat_arith

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}