--- 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 *)
--- 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)"