| changeset 55143 | 04448228381d |
| parent 55088 | 57c82e01022b |
| child 55242 | 413ec965f95d |
--- a/src/HOL/Set_Interval.thy Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Set_Interval.thy Sat Jan 25 22:06:07 2014 +0100 @@ -728,7 +728,7 @@ qed auto lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}" -by(auto intro!: image_eqI[where x="nat x", standard]) + by (auto intro!: image_eqI [where x = "nat x" for x]) context ordered_ab_group_add begin