changeset 54864 | a064732223ad |
parent 54863 | 82acc20ded73 |
child 67406 | 23307fd33906 |
--- a/src/HOL/IMP/Sec_Typing.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/IMP/Sec_Typing.thy Wed Dec 25 17:39:07 2013 +0100 @@ -200,7 +200,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 less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')