| Wed, 20 Dec 2023 20:48:57 +0100 | wenzelm | tuned names; | changeset | files |
| Wed, 20 Dec 2023 20:28:55 +0100 | wenzelm | more informative exceptions; | changeset | files |
| 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 |