HomeIsabelle/Phabricator

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

Authored by makarius.

Description

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

Details

Committed
makariusDec 1 2019, 3:38 PM
Parents
rISABELLE95e12ecdcb5f: proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o…
Branches
Unknown
Tags
Unknown