| Thu, 05 Nov 2009 15:44:39 +0100 |
boehmes |
merged
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 15:24:49 +0100 |
boehmes |
handle let expressions inside terms by unfolding (instead of raising an exception),
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:48:40 +0100 |
boehmes |
shorter names for variables and verification conditions,
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:37:39 +0100 |
wenzelm |
more accurate dependencies;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 17:17:30 +0100 |
krauss |
added Tree23 to IsaMakefile
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 17:54:24 +0100 |
boehmes |
added HOL-Boogie
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 13:59:49 +0100 |
haftmann |
moved Commutative_Ring into session Decision_Procs
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 01:32:06 +0100 |
krauss |
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 18:17:26 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:06:15 +0100 |
wenzelm |
separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 08:14:39 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| 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
|