# HG changeset patch
# User huffman
# Date 1330098929 -3600
# Node ID 134b74908a8e6f5d81dd8e484120db3955065b49
# Parent  a557db8f2fbfba9de24c31498ccaa9bffc76b940
avoid using Int.succ or Int.pred in proofs

diff -r a557db8f2fbf -r 134b74908a8e src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Feb 24 16:53:59 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 24 16:55:29 2012 +0100
@@ -1598,7 +1598,7 @@
   apply (unfold word_succ_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
-  apply (simp add: to_bl_def rbl_succ Int.succ_def)
+  apply (simp add: to_bl_def rbl_succ)
   done
 
 lemma word_pred_rbl:
@@ -1606,7 +1606,7 @@
   apply (unfold word_pred_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
-  apply (simp add: to_bl_def rbl_pred Int.pred_def)
+  apply (simp add: to_bl_def rbl_pred)
   done
 
 lemma word_add_rbl: