| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
tuned fact references
|
changeset |
files
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
clarified library contents
|
changeset |
files
|
| Sat, 17 Dec 2016 15:22:13 +0100 |
haftmann |
standardized notation
|
changeset |
files
|
| Sat, 17 Dec 2016 15:22:00 +0100 |
haftmann |
redundant
|
changeset |
files
|
| Sat, 17 Dec 2016 15:22:00 +0100 |
haftmann |
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
|
changeset |
files
|
| Sat, 17 Dec 2016 15:22:00 +0100 |
haftmann |
added lemmas demanded by FIXMEs
|
changeset |
files
|
| Sat, 17 Dec 2016 15:22:00 +0100 |
haftmann |
dropped comment after conversation with author: predicate compiler works independently from any code generator setup
|
changeset |
files
|
| Sat, 17 Dec 2016 14:47:41 +0100 |
wenzelm |
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
|
changeset |
files
|
| Sat, 17 Dec 2016 14:13:15 +0100 |
wenzelm |
tuned signature -- suppress pointless exports;
|
changeset |
files
|
| Sat, 17 Dec 2016 14:09:39 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Dec 2016 14:04:05 +0100 |
wenzelm |
more standard pretty printing;
|
changeset |
files
|
| Sat, 17 Dec 2016 13:42:25 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Dec 2016 12:24:13 +0100 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Fri, 16 Dec 2016 22:54:14 +0100 |
blanchet |
refactored induction principle generation code, for reuse for nonuniform datatypes
|
changeset |
files
|
| Fri, 16 Dec 2016 19:50:46 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 16 Dec 2016 19:07:16 +0100 |
wenzelm |
consolidate nested thms with persistent result, for improved performance;
|
changeset |
files
|