# HG changeset patch
# User haftmann
# Date 1594875145 0
# Node ID 587d4681240c21703aaf7a9b659bd8d0191201dd
# Parent  7b112eedc8598223bf2d38fa2c9003dd0228768b
yet another alias

diff -r 7b112eedc859 -r 587d4681240c NEWS
--- a/NEWS	Wed Jul 15 20:06:45 2020 +0200
+++ b/NEWS	Thu Jul 16 04:52:25 2020 +0000
@@ -75,8 +75,8 @@
 into its components "drop_bit" and "take_bit".  INCOMPATIBILITY.
 
 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
-"bintrunc", "sbintrunc", "bin_cat" and "max_word" are now mere
-input abbreviations.  Minor INCOMPATIBILITY.
+"bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now
+mere input abbreviations.  Minor INCOMPATIBILITY.
 
 * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
 Minor INCOMPATIBILITY.
diff -r 7b112eedc859 -r 587d4681240c src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Wed Jul 15 20:06:45 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Thu Jul 16 04:52:25 2020 +0000
@@ -246,6 +246,9 @@
 abbreviation (input) sbintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>sbintrunc \<equiv> signed_take_bit\<close>
 
+abbreviation (input) norm_sint :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>norm_sint n \<equiv> signed_take_bit (n - 1)\<close>
+
 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n"
   by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift)
   
diff -r 7b112eedc859 -r 587d4681240c src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Jul 15 20:06:45 2020 +0200
+++ b/src/HOL/Word/Word.thy	Thu Jul 16 04:52:25 2020 +0000
@@ -80,9 +80,6 @@
 definition unats :: "nat \<Rightarrow> nat set"
   where "unats n = {i. i < 2 ^ n}"
 
-definition norm_sint :: "nat \<Rightarrow> int \<Rightarrow> int"
-  where "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
-
 definition scast :: "'a::len word \<Rightarrow> 'b::len word"
   \<comment> \<open>cast a word to a different length\<close>
   where "scast w = word_of_int (sint w)"