--- a/src/HOL/Word/BinGeneral.thy Fri Aug 28 19:35:49 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy Fri Aug 28 19:43:19 2009 +0200
@@ -493,7 +493,7 @@
lemma sbintrunc_sbintrunc_l:
"n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
- by (rule bin_eqI) (auto simp: nth_sbintr min_def)
+ by (rule bin_eqI) (auto simp: nth_sbintr)
lemma bintrunc_bintrunc_ge:
"n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
@@ -501,14 +501,12 @@
lemma bintrunc_bintrunc_min [simp]:
"bintrunc m (bintrunc n w) = bintrunc (min m n) w"
- apply (unfold min_def)
apply (rule bin_eqI)
apply (auto simp: nth_bintr)
done
lemma sbintrunc_sbintrunc_min [simp]:
"sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
- apply (unfold min_def)
apply (rule bin_eqI)
apply (auto simp: nth_sbintr)
done