changeset 57512 | cc97b347b301 |
parent 56927 | 4044a7d1720f |
child 58249 | 180f1b3508ed |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri Jul 04 20:07:08 2014 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri Jul 04 20:18:47 2014 +0200 @@ -193,7 +193,7 @@ proof case goal1 thus ?case by(auto simp add: filter_plus_ivl_def) - (metis rep_minus_ivl add_diff_cancel add_commute)+ + (metis rep_minus_ivl add_diff_cancel add.commute)+ next case goal2 thus ?case by(cases a1, cases a2,