HomeIsabelle/Phabricator

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

Authored by makarius.

Description

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

Details

Committed
makariusNov 30 2019, 4:46 PM
Parents
rISABELLEabb0d984abbc: tuned -- avoid confusion of fun_t with fun_lhs;
Branches
Unknown
Tags
Unknown