Sun, 17 Dec 2023 22:57:20 +0100 | wenzelm | proper Thm.transfer (required for zproofs); | changeset | files |
Sun, 17 Dec 2023 21:43:14 +0100 | wenzelm | clarified signature; | changeset | files |
Sun, 17 Dec 2023 21:34:44 +0100 | wenzelm | proper beta_norm after instantiation (amending 90c5aadcc4b2); | changeset | files |
Sun, 17 Dec 2023 21:30:21 +0100 | wenzelm | minor performance tuning: more direct beta_norm; | changeset | files |
Sun, 17 Dec 2023 21:12:18 +0100 | wenzelm | more robust norm_proof: turn env into instantiation, based on visible statement; | changeset | files |
Sun, 17 Dec 2023 15:09:55 +0100 | wenzelm | proper scope of cache (amending 61af3e917597); | changeset | files |
Sun, 17 Dec 2023 11:15:08 +0100 | wenzelm | tuned comments; | changeset | files |