#67 (Feb 17, 2016, 11:22:25 PM)

1. minimum of maintainability for proof (detail / hgweb)
2. tuned proofs (detail / hgweb)
3. dropped various legacy fact bindings and tuned proofs (detail / hgweb)
4. separated potentially conflicting type class instance into separate theory (detail / hgweb)
5. accommodated gcd instances for polynomials (detail / hgweb)
6. more sophisticated GCD syntax (detail / hgweb)
7. dropped various legacy fact bindings (detail / hgweb)
8. prefer abbreviations for compound operators INFIMUM and SUPREMUM (detail / hgweb)

Started by an SCM change