| 2020-02-15 |
wenzelm |
NEWS;
|
changeset |
files
|
| 2020-02-14 |
wenzelm |
Added tag Isabelle2020-RC0 for changeset 21c0b3a9d2f8
|
changeset |
files
|
| 2020-02-13 |
nipkow |
added lemmas
|
changeset |
files
|
| 2020-02-13 |
haftmann |
canonical approach towards lifting
|
changeset |
files
|
| 2020-02-11 |
haftmann |
more instances
|
changeset |
files
|
| 2020-02-11 |
haftmann |
tuned proof
|
changeset |
files
|
| 2020-02-12 |
wenzelm |
afford newer Mercurial version, just before odd problems in 4.0 and 4.1;
|
changeset |
files
|
| 2020-02-12 |
wenzelm |
afford more logging (following defaults on Ubuntu);
|
changeset |
files
|
| 2020-02-11 |
wenzelm |
updated for release;
|
changeset |
files
|
| 2020-02-11 |
wenzelm |
tuned;
|
changeset |
files
|
| 2020-02-11 |
wenzelm |
updated for release;
|
changeset |
files
|
| 2020-02-11 |
paulson |
some lemmas about the lex ordering on lists, etc.
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
proper symbols;
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
NEWS;
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
recover from Unicode accident in 4abd07cd034f;
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
updated for release;
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
NEWS;
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
NEWS;
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
tuned;
|
changeset |
files
|
| 2020-02-10 |
wenzelm |
tuned;
|
changeset |
files
|
| 2020-02-09 |
haftmann |
easy abstraction over pointwise bit operations
|
changeset |
files
|
| 2020-02-09 |
haftmann |
more rules for natural deduction from inequalities
|
changeset |
files
|
| 2020-02-09 |
haftmann |
rule concerning bit (push_bit ...)
|
changeset |
files
|
| 2020-02-09 |
haftmann |
more lemmas
|
changeset |
files
|
| 2020-02-08 |
wenzelm |
allow to override repository versions at runtime;
|
changeset |
files
|
| 2020-02-07 |
wenzelm |
follow Phabricator update 2020 Week 5;
|
changeset |
files
|
| 2020-02-05 |
haftmann |
simplified logical constructions
|
changeset |
files
|
| 2020-02-05 |
haftmann |
simplified logical constructions
|
changeset |
files
|
| 2020-02-03 |
haftmann |
more theorems
|
changeset |
files
|
| 2020-02-04 |
paulson |
Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf
|
changeset |
files
|
| 2020-02-04 |
nipkow |
tuned
|
changeset |
files
|
| 2020-02-03 |
nipkow |
tuned
|
changeset |
files
|
| 2020-02-03 |
nipkow |
added Interval_Tree.thy
|
changeset |
files
|
| 2020-02-01 |
haftmann |
more specific class assumptions
|
changeset |
files
|
| 2020-02-01 |
haftmann |
more theorems
|
changeset |
files
|
| 2020-01-28 |
wenzelm |
ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9);
|
changeset |
files
|
| 2020-01-28 |
paulson |
Tidied up some messy proofs
|
changeset |
files
|
| 2020-01-26 |
haftmann |
sketches of ideas still to come
|
changeset |
files
|
| 2020-01-26 |
haftmann |
more theorems
|
changeset |
files
|
| 2020-01-26 |
haftmann |
generalized
|
changeset |
files
|
| 2020-01-26 |
haftmann |
tuned
|
changeset |
files
|
| 2020-01-27 |
paulson |
Two lemmas about nsets
|
changeset |
files
|
| 2020-01-27 |
paulson |
A few lemmas connected with orderings
|
changeset |
files
|
| 2020-01-22 |
haftmann |
tuned
|
changeset |
files
|
| 2020-01-22 |
haftmann |
tuned
|
changeset |
files
|
| 2020-01-22 |
haftmann |
dropped dead code
|
changeset |
files
|
| 2020-01-22 |
nipkow |
merged
|
changeset |
files
|
| 2020-01-22 |
nipkow |
added lemma
|
changeset |
files
|
| 2020-01-21 |
Manuel Eberl |
Removed multiplicativity assumption from normalization_semidom
|
changeset |
files
|
| 2020-01-19 |
wenzelm |
clarified file names;
|
changeset |
files
|
| 2020-01-19 |
wenzelm |
clarified build_polyml_component: include IDE entry point for ML compiler;
|
changeset |
files
|
| 2020-01-19 |
wenzelm |
merged
|
changeset |
files
|
| 2020-01-17 |
wenzelm |
tuned spelling;
|
changeset |
files
|
| 2020-01-19 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
changeset |
files
|
| 2020-01-17 |
Manuel Eberl |
Removed unnecessary and problematic trivial lemma from HOL-Algebra
|
changeset |
files
|
| 2020-01-16 |
wenzelm |
proper executable file;
|
changeset |
files
|
| 2020-01-16 |
wenzelm |
more documentation: odd option for special situations;
|
changeset |
files
|
| 2020-01-16 |
wenzelm |
tuned;
|
changeset |
files
|
| 2020-01-16 |
wenzelm |
updated to sumatra_pdf-3.1.2-1: x86_64-windows;
|
changeset |
files
|
| 2020-01-16 |
wenzelm |
updated to stack-2.1.3, stackage lts-13.19, ghc-8.6.4;
|
changeset |
files
|