| Tue, 06 Aug 2019 17:26:40 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 06 Aug 2019 16:29:28 +0200 |
wenzelm |
more robust and convenient treatment of implicit context;
|
changeset |
files
|
| Tue, 06 Aug 2019 16:15:22 +0200 |
wenzelm |
clarified context: proper transfer;
|
changeset |
files
|
| Tue, 06 Aug 2019 16:13:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 05 Aug 2019 16:11:43 +0200 |
wenzelm |
clarified modules: more direct data implementation;
|
changeset |
files
|
| Tue, 06 Aug 2019 18:04:06 +0200 |
Manuel Eberl |
Added Takeuchi function to HOL-ex
|
changeset |
files
|
| Mon, 05 Aug 2019 11:20:56 +0200 |
wenzelm |
full AFP test on lrzcloud2;
|
changeset |
files
|
| Mon, 05 Aug 2019 11:08:50 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sat, 03 Aug 2019 21:18:12 +0200 |
wenzelm |
more efficient data structure;
|
changeset |
files
|
| Sat, 03 Aug 2019 20:30:24 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 03 Aug 2019 16:17:16 +0200 |
wenzelm |
guard constraints by record_proofs=1, until performance implications have become more clear;
|
changeset |
files
|
| Sat, 03 Aug 2019 16:10:34 +0200 |
wenzelm |
more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;
|
changeset |
files
|