# HG changeset patch
# User wenzelm
# Date 1678226894 -3600
# Node ID 13b53fae16f3793f6eddbe9de8cfa278772987a7
# Parent  b975f5aaf6b80459e319cd7924ebc8e769c7e13d
tuned whitespace;

diff -r b975f5aaf6b8 -r 13b53fae16f3 src/HOL/ex/Note_on_signed_division_on_words.thy
--- a/src/HOL/ex/Note_on_signed_division_on_words.thy	Tue Mar 07 23:02:52 2023 +0100
+++ b/src/HOL/ex/Note_on_signed_division_on_words.thy	Tue Mar 07 23:08:14 2023 +0100
@@ -6,21 +6,21 @@
 
 context semiring_bit_operations
 begin
-	
+
 lemma take_bit_Suc_from_most:
   \<open>take_bit (Suc n) a = 2 ^ n * of_bool (bit a n) OR take_bit n a\<close>
   by (rule bit_eqI) (auto simp add: bit_simps less_Suc_eq)
-	
+
 end
-	
+
 context ring_bit_operations
 begin
-	
+
 lemma signed_take_bit_exp_eq_int:
   \<open>signed_take_bit m (2 ^ n) =
     (if n < m then 2 ^ n else if n = m then - (2 ^ n) else 0)\<close>
   by (rule bit_eqI) (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
-	
+
 end
 
 lift_definition signed_divide_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wdiv\<close> 70)
@@ -46,5 +46,5 @@
       by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_rmod)
   qed
 qed
-  
+
 end