| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
generate useful information for type axioms
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
updated FAQ
|
changeset |
files
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
more informative message when Sledgehammer finds an unsound proof
|
changeset |
files
|
| Fri, 20 May 2011 12:35:44 +0200 |
haftmann |
tuned proofs
|
changeset |
files
|
| Fri, 20 May 2011 12:09:54 +0200 |
haftmann |
NEWS
|
changeset |
files
|
| Fri, 20 May 2011 12:07:17 +0200 |
haftmann |
point-free characterization of operations on finite sets
|
changeset |
files
|
| Fri, 20 May 2011 11:44:34 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 20 May 2011 11:44:16 +0200 |
haftmann |
names of fold_set locales resemble name of characteristic property more closely
|
changeset |
files
|
| Fri, 20 May 2011 09:31:36 +0200 |
krauss |
clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton
|
changeset |
files
|
| Fri, 20 May 2011 08:16:56 +0200 |
haftmann |
use point-free characterization for locale fun_left_comm_idem
|
changeset |
files
|
| Fri, 20 May 2011 08:16:13 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
| Tue, 17 May 2011 15:00:39 +0200 |
hoelzl |
Collect intro-rules for sigma-algebras
|
changeset |
files
|
| Tue, 17 May 2011 14:36:54 +0200 |
hoelzl |
the measurable sets with null measure form a ring
|
changeset |
files
|