| Wed, 20 Dec 2023 14:26:18 +0100 | wenzelm | more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy"); | changeset | files |
| Wed, 20 Dec 2023 12:50:38 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 20 Dec 2023 12:50:33 +0100 | wenzelm | more informative exception; | changeset | files |
| Wed, 20 Dec 2023 12:50:16 +0100 | wenzelm | clarified signature; | changeset | files |
| Wed, 20 Dec 2023 11:55:04 +0100 | wenzelm | clarified ML toplevel output: avoid "??." prefix; | changeset | files |
| Wed, 20 Dec 2023 11:16:39 +0100 | wenzelm | tuned; | changeset | files |
| Tue, 19 Dec 2023 23:06:26 +0100 | wenzelm | merged | changeset | files |