Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(re-)added simp rules for (_ + _) div/mod _
authorhaftmann
Mon, 21 Jul 2008 16:30:49 +0200
changeset 27677 646ea25ff59d
parent 27676 55676111ed69
child 27678 85ea2be46c71
(re-)added simp rules for (_ + _) div/mod _
src/HOL/Word/BinBoolList.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle