| Tue, 13 Nov 2012 09:08:32 +0100 |
haftmann |
prefer explicit Random.seed
|
changeset |
files
|
| Mon, 12 Nov 2012 23:24:40 +0100 |
haftmann |
dropped dead code
|
changeset |
files
|
| Mon, 12 Nov 2012 23:24:40 +0100 |
haftmann |
tuned import order
|
changeset |
files
|
| Mon, 12 Nov 2012 18:42:49 +0100 |
nipkow |
tuned layout
|
changeset |
files
|
| Mon, 12 Nov 2012 14:46:42 +0100 |
blanchet |
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
|
changeset |
files
|
| Mon, 12 Nov 2012 14:11:51 +0100 |
blanchet |
create temp directory if not already created
|
changeset |
files
|
| Mon, 12 Nov 2012 12:28:19 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 12 Nov 2012 12:27:58 +0100 |
nipkow |
new theory IMP/Finite_Reachable
|
changeset |
files
|
| Mon, 12 Nov 2012 12:06:56 +0100 |
blanchet |
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
|
changeset |
files
|
| Mon, 12 Nov 2012 11:52:37 +0100 |
blanchet |
centralized term printing code
|
changeset |
files
|
| Mon, 12 Nov 2012 11:32:22 +0100 |
blanchet |
thread context correctly when printing backquoted facts
|
changeset |
files
|
| Sun, 11 Nov 2012 19:56:02 +0100 |
haftmann |
dropped dead code;
|
changeset |
files
|
| Sun, 11 Nov 2012 19:24:01 +0100 |
haftmann |
modernized, simplified and compacted oracle and proof method glue code;
|
changeset |
files
|
| Fri, 09 Nov 2012 19:21:47 +0100 |
nipkow |
merged
|
changeset |
files
|
| Fri, 09 Nov 2012 19:16:31 +0100 |
nipkow |
fixed underscores
|
changeset |
files
|
| Fri, 09 Nov 2012 14:31:26 +0100 |
immler |
moved lemmas into projective_family; added header for theory Projective_Family
|
changeset |
files
|
| Fri, 09 Nov 2012 14:14:45 +0100 |
immler |
removed redundant/unnecessary assumptions from projective_family
|
changeset |
files
|
| Wed, 07 Nov 2012 14:41:49 +0100 |
immler |
assume probability spaces; allow empty index set
|
changeset |
files
|
| Wed, 07 Nov 2012 11:33:27 +0100 |
immler |
added projective_family; generalized generator in product_prob_space to projective_family
|
changeset |
files
|
| Tue, 06 Nov 2012 11:03:28 +0100 |
immler |
moved lemmas further up
|
changeset |
files
|
| Thu, 08 Nov 2012 20:02:41 +0100 |
bulwahn |
tuned proofs
|
changeset |
files
|
| Thu, 08 Nov 2012 19:55:37 +0100 |
bulwahn |
using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier
|
changeset |
files
|
| Thu, 08 Nov 2012 19:55:35 +0100 |
bulwahn |
hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call
|
changeset |
files
|
| Thu, 08 Nov 2012 19:55:19 +0100 |
bulwahn |
NEWS
|
changeset |
files
|