| Sun, 10 Jul 2016 22:05:18 +0200 |
Lars Hupel |
tuned
|
changeset |
files
|
| Sat, 09 Jul 2016 13:26:16 +0200 |
haftmann |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
|
changeset |
files
|
| Fri, 08 Jul 2016 23:43:11 +0200 |
haftmann |
avoid to hide equality behind (output) abbreviation
|
changeset |
files
|
| Fri, 08 Jul 2016 23:43:11 +0200 |
haftmann |
default rule for single-step reasoning
|
changeset |
files
|
| Fri, 08 Jul 2016 19:35:31 +0200 |
nipkow |
new style dummy_pats
|
changeset |
files
|
| Fri, 08 Jul 2016 16:38:31 +0200 |
nipkow |
added path_len
|
changeset |
files
|
| Thu, 07 Jul 2016 18:08:10 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 07 Jul 2016 18:08:02 +0200 |
nipkow |
got rid of class cmp; added height-size proofs by Daniel Stuewe
|
changeset |
files
|
| Thu, 07 Jul 2016 17:34:39 +0200 |
fleury |
more instantiations for multiset
|
changeset |
files
|
| Thu, 07 Jul 2016 09:24:03 +0200 |
blanchet |
moved lemmas and locales around (with minor incompatibilities)
|
changeset |
files
|
| Thu, 07 Jul 2016 00:43:27 +0200 |
blanchet |
updated example
|
changeset |
files
|
| Wed, 06 Jul 2016 23:19:28 +0200 |
blanchet |
leverage new 'order' type class instantiation in multiset
|
changeset |
files
|
| Wed, 06 Jul 2016 23:19:27 +0200 |
blanchet |
updated examples
|
changeset |
files
|
| Wed, 06 Jul 2016 22:52:10 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 06 Jul 2016 20:19:51 +0200 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Wed, 06 Jul 2016 14:09:13 +0200 |
wenzelm |
proper signature;
|
changeset |
files
|
| Wed, 06 Jul 2016 11:29:51 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 06 Jul 2016 13:45:52 +0200 |
Lars Hupel |
simplify build scripts
|
changeset |
files
|
| Tue, 05 Jul 2016 23:39:49 +0200 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Tue, 05 Jul 2016 22:47:48 +0200 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Tue, 05 Jul 2016 22:23:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 05 Jul 2016 21:23:21 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 05 Jul 2016 20:51:02 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
changeset |
files
|
| Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
changeset |
files
|
| Tue, 05 Jul 2016 10:32:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 05 Jul 2016 20:29:58 +0200 |
hoelzl |
Probability: simplified Levy's uniqueness theorem
|
changeset |
files
|
| Tue, 05 Jul 2016 18:00:21 +0200 |
blanchet |
avoid reference to invisible theorem, by using another one instead (suggested by Anders Schlichtkrull; the document's author is incomunicado)
|
changeset |
files
|
| Tue, 05 Jul 2016 17:52:08 +0200 |
blanchet |
tuning
|
changeset |
files
|