| Fri, 29 Oct 2021 11:59:02 +0200 | wenzelm | avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570); | changeset | files |
| Fri, 29 Oct 2021 11:57:49 +0200 | wenzelm | added Thm.instantiate_beta; | changeset | files |
| Thu, 28 Oct 2021 06:39:36 +0000 | haftmann | moved generic implementation into HOL-Main | changeset | files |
| Fri, 29 Oct 2021 00:01:14 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 28 Oct 2021 23:44:31 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 28 Oct 2021 23:37:53 +0200 | wenzelm | clarified antiquotations; | changeset | files |
| Thu, 28 Oct 2021 21:28:52 +0200 | wenzelm | clarified antiquotations; | changeset | files |