Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Word/Bit_Int.thy
changeset 45529 0e1037d4e049
parent 45475 b2b087c20e45
child 45543 827bf668c822 
--- a/src/HOL/Word/Bit_Int.thy	Wed Nov 16 12:29:50 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Wed Nov 16 13:58:31 2011 +0100
@@ -657,7 +657,7 @@
 lemma bin_split_num:
   "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   apply (induct n, clarsimp)
-  apply (simp add: bin_rest_div zdiv_zmult2_eq)
+  apply (simp add: bin_rest_def zdiv_zmult2_eq)
   apply (case_tac b rule: bin_exhaust)
   apply simp
   apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def
isabelle