| Tue, 17 Mar 2015 15:11:25 +0000 | paulson | more general type class for factorial. Now allows code generation (?) | file | diff | annotate |
| Mon, 16 Mar 2015 15:30:00 +0000 | paulson | The factorial function, "fact", now has type "nat => 'a" | file | diff | annotate |
| Tue, 10 Mar 2015 16:12:35 +0000 | paulson | renaming HOL/Fact.thy -> Binomial.thy | file | diff | annotate | base |
| Wed, 26 Jul 2006 19:23:04 +0200 | webertj | linear arithmetic splits certain operators (e.g. min, max, abs) | file | diff | annotate |
| Fri, 17 Mar 2006 10:04:27 +0100 | ballarin | Renamed setsum_mult to setsum_right_distrib. | file | diff | annotate |
| Tue, 20 Sep 2005 14:03:37 +0200 | wenzelm | tuned theory dependencies; | file | diff | annotate |
| Thu, 07 Jul 2005 12:36:56 +0200 | nipkow | Used to be part of Finite_Set (or was it SetInterval?) | file | diff | annotate |