spurious proof failure
authorhaftmann
Wed, 22 Jul 2009 14:20:31 +0200
changeset 32133 b513db807fca
parent 32129 d2aea34845d4
child 32134 ee143615019c
spurious proof failure
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 *}