--- a/src/HOL/MicroJava/BV/LBVSpec.thy Wed Aug 04 19:09:41 2004 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Wed Aug 04 19:09:58 2004 +0200
@@ -301,7 +301,7 @@
proof -
from pc have "0 < length (drop pc is)" by simp
then obtain i r where Cons: "drop pc is = i#r"
- by (auto simp add: neq_Nil_conv simp del: length_drop)
+ by (auto simp add: neq_Nil_conv simp del: length_drop drop_eq_Nil)
hence "i#r = drop pc is" ..
with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp
from pc have "is!pc = drop pc is ! 0" by simp
--- a/src/HOL/NumberTheory/Finite2.thy Wed Aug 04 19:09:41 2004 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy Wed Aug 04 19:09:58 2004 +0200
@@ -266,13 +266,7 @@
lemma sum_prop [rule_format]: "finite B ==>
inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B";
-apply (rule finite_induct, assumption, force)
-apply (rule impI, auto)
-apply (simp add: inj_on_def)
-apply (subgoal_tac "f x \<notin> f ` F")
-apply (subgoal_tac "finite (f ` F)");
-apply (auto simp add: setsum_insert)
-by (simp add: inj_on_def)
+by (rule finite_induct, auto)
lemma sum_prop_id: "finite B ==> inj_on f B ==>
setsum f B = setsum id (f ` B)";