changeset 16733 | 236dfafbeb63 |
parent 16417 | 9bc16273c2d4 |
child 27651 | 16a26996c30e |
16732:1bbe526a552c | 16733:236dfafbeb63 |
---|---|
226 apply simp+ |
226 apply simp+ |
227 apply(rule Basic) |
227 apply(rule Basic) |
228 apply simp |
228 apply simp |
229 apply clarify |
229 apply clarify |
230 apply simp |
230 apply simp |
231 apply(force elim:Example2_lemma2_Suc0) |
231 apply(simp add:Example2_lemma2_Suc0 cong:if_cong) |
232 apply simp+ |
232 apply simp+ |
233 done |
233 done |
234 |
234 |
235 subsection {* Find Least Element *} |
235 subsection {* Find Least Element *} |
236 |
236 |