Fri, 22 Jul 2016 11:00:43 +0200 | wenzelm | tuned proofs -- avoid unstructured calculation; | file | diff | annotate |
Mon, 25 Apr 2016 16:09:26 +0200 | wenzelm | eliminated old 'def'; | 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 |
Tue, 16 Jun 2015 11:31:22 +0200 | hoelzl | tuned src/HOL/ex/Ballot | 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 |