proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";