Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 18:21:02 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 11:43:06 +0000 |
paulson |
merged
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 11:42:31 +0000 |
paulson |
New theory Probability, which contains a development of measure theory
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 14:46:03 +0000 |
paulson |
merged
|
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, 27 Oct 2009 19:03:59 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 09:03:56 +0100 |
bulwahn |
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 18:09:11 +0100 |
boehmes |
removed unused file smt_builtin.ML,
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 20:04:20 +0100 |
wenzelm |
recovered sort indentation for "sort position", as documented in the file;
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 14:57:49 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 14:21:20 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 09:14:29 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 18:59:24 +0200 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|
Thu, 22 Oct 2009 14:51:47 +0200 |
blanchet |
added Nitpick's theory and ML files to Isabelle/HOL;
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 14:54:43 +0100 |
berghofe |
merged
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 14:53:33 +0100 |
berghofe |
Added Pattern.thy to Nominal/Examples.
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 11:30:08 +0100 |
wenzelm |
more precise dependencies, notably for HOL-Multivariate_Analysis;
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 09:03:57 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 13:23:18 +0200 |
himmelma |
distinguished session for multivariate analysis
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 16:37:56 +0200 |
krauss |
renamed auto_term.ML -> relation.ML
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 16:22:10 +0200 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 15:33:19 +0200 |
krauss |
renamed FundefDatatype -> Function_Fun
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 17:12:47 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 17:12:36 +0200 |
haftmann |
turned off old quickcheck
|
file |
diff |
annotate
|
Fri, 23 Oct 2009 14:33:07 +0200 |
krauss |
pat_completeness gets its own file
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 20:03:23 +0200 |
wenzelm |
modernized session SET_Protocol;
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 19:52:04 +0200 |
wenzelm |
modernized session Metis_Examples;
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 19:37:09 +0200 |
wenzelm |
modernized session Isar_Examples;
|
file |
diff |
annotate
|