| Thu, 04 Apr 2024 15:29:41 +0200 | Manuel Eberl | moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory | file | diff | annotate |
| Tue, 21 Jan 2020 11:02:27 +0100 | Manuel Eberl | Removed multiplicativity assumption from normalization_semidom | file | diff | annotate |
| Sat, 09 Mar 2019 13:24:59 +0100 | wenzelm | tuned proof; | file | diff | annotate |
| Mon, 24 Sep 2018 14:30:09 +0200 | nipkow | Prefix form of infix with * on either side no longer needs special treatment | file | diff | annotate |