HomeIsabelle/Phabricator

proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o…

Description

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

Details

Provenance
makariusAuthored on
Parents
rISABELLEabb0d984abbc: tuned -- avoid confusion of fun_t with fun_lhs;
Branches
Unknown
Tags
Unknown