| Tue, 12 Dec 2006 07:11:58 +0100 | huffman | fix assumptions on NSDERIV_quotient | file | diff | annotate |
| Tue, 12 Dec 2006 04:37:25 +0100 | huffman | changed (ns)deriv to take functions of type 'a::real_normed_field => 'a | file | diff | annotate |
| Fri, 17 Nov 2006 02:20:03 +0100 | wenzelm | more robust syntax for definition/abbreviation/notation; | file | diff | annotate |
| Wed, 08 Nov 2006 02:13:02 +0100 | huffman | LIM_compose -> isCont_LIM_compose; | file | diff | annotate |
| Tue, 07 Nov 2006 09:33:47 +0100 | krauss | * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. | file | diff | annotate |
| Sat, 04 Nov 2006 00:11:11 +0100 | huffman | new Deriv.thy contains stuff from Lim.thy | file | diff | annotate |