| Sat, 02 Jul 2016 20:22:25 +0200 | haftmann | simplified definitions of combinatorial functions | 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 |
| Fri, 13 Nov 2015 12:27:13 +0000 | paulson | Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes. | 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 |
| Tue, 06 Oct 2015 17:47:28 +0200 | wenzelm | isabelle update_cartouches; | file | diff | annotate |
| Fri, 12 Jun 2015 10:33:02 +0200 | bulwahn | add examples from Freek's top 100 theorems (thms 30, 73, 77) | file | diff | annotate |