HomeIsabelle/Phabricator

more informative spec rules: optional name;

Authored by makarius.

Description

more informative spec rules: optional name;
clarified signature;
more thorough treatment of Thm.trim_context vs. Thm.transfer;

Details

Committed
makariusNov 29 2019, 8:57 PM
Parents
rISABELLEc7d4f2ab40b9: proper theory context, e.g. for Thm.transfer;
Branches
Unknown
Tags
Unknown