# HG changeset patch
# User wenzelm
# Date 1392209803 -3600
# Node ID db691cc7928900ab16a54e48b982310959d64dd7
# Parent  3b95e70c5cb3b2e59294089a7469c10c0530fe92
eliminated hard tabs (assuming tab-width=2);

diff -r 3b95e70c5cb3 -r db691cc79289 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Feb 12 13:53:11 2014 +0100
+++ b/src/HOL/Divides.thy	Wed Feb 12 13:56:43 2014 +0100
@@ -1968,13 +1968,13 @@
 lemma [simp]:
   shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
     and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"
-	  and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
-	  and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
-	  and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
-	  and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
+    and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
+    and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
+    and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
+    and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
   by (simp_all del: arith_special
     add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)
-	
+
 lemma [simp]:
   shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"
     and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"