replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
@Article{Berger-JAR-2001,
author = {Ulrich Berger and Helmut Schwichtenberg and Monika Seisenberger},
title = {The {Warshall} Algorithm and {Dickson's} Lemma: Two
Examples of Realistic Program Extraction},
journal = {Journal of Automated Reasoning},
publisher = {Kluwer Academic Publishers},
year = 2001,
volume = 26,
pages = {205--221}
}
@TechReport{Coquand93,
author = {Thierry Coquand and Daniel Fridlender},
title = {A proof of {Higman's} lemma by structural induction},
institution = {Chalmers University},
year = 1993,
month = {November}
}