| Fri, 25 Sep 2020 14:11:48 +0100 | paulson | fixed some remarkably ugly proofs | file | diff | annotate |
| Sun, 29 Jul 2018 23:04:22 +0100 | paulson | de-applying and removal of obsolete aliases | file | diff | annotate |
| Sun, 15 Jul 2018 13:15:31 +0100 | paulson | more de-applying and a fix | file | diff | annotate |
| Sat, 14 Jul 2018 22:32:15 +0100 | paulson | de-applying | file | diff | annotate |
| Sun, 20 May 2018 11:57:17 +0200 | wenzelm | prefer HTTPS; | file | diff | annotate |
| Sat, 02 Dec 2017 16:50:53 +0000 | haftmann | more simplification rules | file | diff | annotate |
| Fri, 20 Oct 2017 20:57:55 +0200 | haftmann | algebraic foundation for congruences | file | diff | annotate |
| Mon, 09 Oct 2017 19:10:48 +0200 | haftmann | tuned proofs | file | diff | annotate |
| Sun, 08 Oct 2017 22:28:20 +0200 | haftmann | avoid fact name clashes | file | diff | annotate |
| Thu, 06 Apr 2017 08:33:37 +0200 | haftmann | more approproiate placement of theories MiscAlgebra and Multiplicate_Group | file | diff | annotate |
| Thu, 06 Apr 2017 21:01:39 +0200 | wenzelm | misc tuning and modernization; | file | diff | annotate |
| Tue, 17 Jan 2017 13:59:10 +0100 | wenzelm | isabelle update_cartouches -c -t; | file | diff | annotate |
| Sat, 17 Dec 2016 15:22:14 +0100 | haftmann | reoriented congruence rules in non-explosive direction | file | diff | annotate |
| Thu, 20 Oct 2016 17:28:09 +0200 | eberlm | Repaired LaTeX in HOL-Data_Structures | file | diff | annotate | base |