| Wed, 01 Dec 2010 20:59:29 +0100 |
nipkow |
moved activation of coercion inference into RealDef and declared function real a coercion.
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 11:32:24 +0100 |
wenzelm |
activate subtyping/coercions in theory Complex_Main;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 20:41:49 +0100 |
hoelzl |
Replaced Integration by Multivariate-Analysis/Real_Integration
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 12:59:57 +0000 |
paulson |
New theory SupInf of the supremum and infimum operators for sets of reals.
|
file |
diff |
annotate
|
| Tue, 19 May 2009 13:57:51 +0200 |
haftmann |
moved Code_Index, Random and Quickcheck before Main
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:16:49 +0200 |
haftmann |
experimental move of Quickcheck and related theories to HOL image
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:16 +0200 |
haftmann |
experimental addition of quickcheck
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:51:39 -0800 |
huffman |
move FrechetDeriv.thy to Library
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 18:14:43 +0100 |
nipkow |
Moved FTA into Lib and cleaned it up a little.
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 00:21:59 +0100 |
wenzelm |
tuned header and description of boot files;
|
file |
diff |
annotate
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 10:23:47 +0100 |
nipkow |
moved ContNotDenum into Library
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|