# HG changeset patch
# User haftmann
# Date 1216650649 -7200
# Node ID 646ea25ff59d6bae45ece05918d8097d401c0aa4
# Parent  55676111ed692fe9701b19d2f1d6a65b6d815ab2
(re-)added simp rules for (_ + _) div/mod _

diff -r 55676111ed69 -r 646ea25ff59d src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Mon Jul 21 15:27:23 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Mon Jul 21 16:30:49 2008 +0200
@@ -1102,7 +1102,7 @@
   apply (case_tac m)
   apply simp
   apply (case_tac "m <= n")
-  apply (auto simp add: div_add_self2)
+  apply auto
   done
 
 lemma bin_rsplit_len: