# HG changeset patch
# User traytel
# Date 1392219358 -3600
# Node ID b445c39cc7e98ffbf7f83fc587b0de38129a5c2c
# Parent  721b4561007a8ec3eb6ef343bd7728e57afdc12d
HOL-IMP fastness

diff -r 721b4561007a -r b445c39cc7e9 src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Wed Feb 12 14:32:45 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Wed Feb 12 16:35:58 2014 +0100
@@ -196,7 +196,7 @@
 lemma strip_pfp_wn:
   "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
 apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
-by (metis (no_types) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)
+by (metis (mono_tags) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)
 
 locale Abs_Int2 = Abs_Int1_mono
 where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"