changeset 33434 | e9de8d69c1b9 |
parent 33318 | ddd97d9dfbfb |
child 35115 | 446c5063e4fd |
--- a/src/HOL/SetInterval.thy Wed Nov 04 09:18:46 2009 +0100 +++ b/src/HOL/SetInterval.thy Wed Nov 04 10:17:43 2009 +0100 @@ -508,7 +508,7 @@ proof(induct A rule:finite_linorder_max_induct) case empty thus ?case by auto next - case (insert A b) + case (insert b A) moreover hence "b ~: A" by auto moreover have "A <= {k..<k+card A}" and "b = k+card A" using `b ~: A` insert by fastsimp+