| Thu, 10 Oct 2019 15:52:30 +0200 | wenzelm | proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation); | changeset | files |
| Thu, 10 Oct 2019 15:18:40 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 10 Oct 2019 15:10:07 +0200 | wenzelm | tuned -- more direct ML expressions; | changeset | files |
| Thu, 10 Oct 2019 15:00:36 +0200 | wenzelm | clarified modules; | changeset | files |
| Thu, 10 Oct 2019 14:55:26 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Thu, 10 Oct 2019 14:53:48 +0200 | wenzelm | more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons; | changeset | files |
| Thu, 10 Oct 2019 11:04:27 +0200 | wenzelm | unused; | changeset | files |