Sun, 01 Dec 2019 21:29:08 +0100 | wenzelm | formal position for spec rule (not significant for equality); | changeset | files |
Sun, 01 Dec 2019 15:38:36 +0100 | wenzelm | proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory"; | changeset | files |