# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 7e353ced895eb330a0099ab097957a14e066f3f9
# Parent  b13e5c3497f588c38980c23c3474742d21f63dc9
rename_tac'd script

diff -r b13e5c3497f5 -r 7e353ced895e src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -314,7 +314,7 @@
 apply(induction e arbitrary: r r' S S')
 apply(auto simp: test_num' Let_def split: option.splits prod.splits)
 apply (metis mono_gamma subsetD)
-apply(drule_tac x = "list" in mono_lookup)
+apply(rename_tac list a b c d, drule_tac x = "list" in mono_lookup)
 apply (metis mono_meet le_trans)
 apply (metis mono_meet mono_lookup mono_update)
 apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)