changeset 54864 | a064732223ad |
parent 54863 | 82acc20ded73 |
child 63539 | 70d4d9e5707b |
--- a/src/HOL/IMP/Sec_TypingT.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/IMP/Sec_TypingT.thy Wed Dec 25 17:39:07 2013 +0100 @@ -190,7 +190,7 @@ apply (metis Skip') apply (metis Assign') apply (metis Seq') -apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono') +apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono') by (metis While')