Fri, 28 Oct 2022 06:34:26 +0000 | haftmann | restructured | file | diff | annotate |
Sun, 21 Aug 2022 06:18:23 +0000 | haftmann | streamlined | file | diff | annotate |
Wed, 17 Feb 2016 21:51:57 +0100 | haftmann | dropped various legacy fact bindings | file | diff | annotate |
Tue, 17 Nov 2015 12:32:08 +0000 | paulson | Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths | file | diff | annotate |
Tue, 10 Nov 2015 14:18:41 +0000 | paulson | Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed. | file | diff | annotate |
Thu, 13 Aug 2015 15:22:11 +0200 | haftmann | qualified adjust_* | file | diff | annotate |