# HG changeset patch
# User haftmann
# Date 1388172932 -3600
# Node ID 0046711700c8b5b44600bdc41535d8f2cc447cd3
# Parent  bab6cade3cc52d99218a83a8439afbf7660e9aab
tuned proofs and declarations

diff -r bab6cade3cc5 -r 0046711700c8 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 14:35:14 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 20:35:32 2013 +0100
@@ -245,7 +245,7 @@
 
 lemma len_bin_to_bl_aux: 
   "length (bin_to_bl_aux n w bs) = n + length bs"
-  by (induct n arbitrary: w bs) auto
+  by (fact size_bin_to_bl_aux)
 
 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
   by (fact size_bin_to_bl) (* FIXME: duplicate *)
diff -r bab6cade3cc5 -r 0046711700c8 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Fri Dec 27 14:35:14 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Fri Dec 27 20:35:32 2013 +0100
@@ -8,7 +8,7 @@
 imports Main Parity
 begin
 
-declare iszero_0 [iff]
+declare iszero_0 [intro]
 
 lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith
   
@@ -25,10 +25,11 @@
 lemma mod_2_neq_1_eq_eq_0:
   fixes k :: int
   shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
-  by arith
+  by (fact not_mod_2_eq_1_eq_0)
 
 lemma z1pmod2:
-  "(2 * b + 1) mod 2 = (1::int)" by arith
+  "(2 * b + 1) mod 2 = (1::int)"
+  by arith
 
 lemma emep1:
   "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
@@ -61,7 +62,7 @@
 
 lemma zless2:
   "0 < (2 :: int)"
-  by arith
+  by (fact zero_less_numeral)
 
 lemma zless2p:
   "0 < (2 ^ n :: int)"