# HG changeset patch # User haftmann # Date 1248265231 -7200 # Node ID b513db807fcad2c698212e7e36d0bda338278da7 # Parent d2aea34845d42176187b9c36187d4326851ff29c spurious proof failure diff -r d2aea34845d4 -r b513db807fca src/HOL/HoareParallel/Mul_Gar_Coll.thy --- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Wed Jul 22 08:05:33 2009 +0200 +++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Wed Jul 22 14:20:31 2009 +0200 @@ -1263,7 +1263,7 @@ apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append) apply force apply clarify -apply(case_tac xa) +apply(case_tac i) apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append) apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt) --{* Collector *}