# HG changeset patch
# User nipkow
# Date 1091639398 -7200
# Node ID bba563cdd99700bc77ab217d39490549878b908b
# Parent  492e5f3a85717f5b7f897651ef9e79965bd33d03
proof mod

diff -r 492e5f3a8571 -r bba563cdd997 src/HOL/MicroJava/BV/LBVSpec.thy
--- 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
diff -r 492e5f3a8571 -r bba563cdd997 src/HOL/NumberTheory/Finite2.thy
--- 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)";