changeset 57512 | cc97b347b301 |
parent 55600 | 3c7610b8dcfc |
child 58249 | 180f1b3508ed |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Fri Jul 04 20:07:08 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Fri Jul 04 20:18:47 2014 +0200 @@ -208,7 +208,7 @@ next case goal2 thus ?case by(auto simp add: filter_plus_ivl_def) - (metis gamma_minus_ivl add_diff_cancel add_commute)+ + (metis gamma_minus_ivl add_diff_cancel add.commute)+ next case goal3 thus ?case by(cases a1, cases a2,