| Mon, 02 Dec 2019 11:57:53 +0100 | wenzelm | tuned comment; | changeset | files |
| Mon, 02 Dec 2019 11:57:42 +0100 | wenzelm | clarified export of spec rules: more like locale; | changeset | files |
| 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 |
| Sat, 30 Nov 2019 16:46:34 +0100 | wenzelm | proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory"; | changeset | files |
| Sat, 30 Nov 2019 16:42:15 +0100 | wenzelm | tuned -- avoid confusion of fun_t with fun_lhs; | changeset | files |