| 2019-12-01 | wenzelm | formal position for spec rule (not significant for equality); | changeset | files |
| 2019-12-01 | wenzelm | proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory"; | changeset | files |
| 2019-11-30 | wenzelm | proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory"; | changeset | files |
| 2019-11-30 | wenzelm | tuned -- avoid confusion of fun_t with fun_lhs; | changeset | files |
| Loading... | |||