HomePhabricator

more robust expose_proofs corresponding to register_proofs/consolidate_theory;

Authored by makarius.

Description

more robust expose_proofs corresponding to register_proofs/consolidate_theory;
expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context;

Details

Committed
makariusNov 4 2019, 2:56 PM
Parents
rISABELLEc85efa2be619: expose derivations more thoroughly, notably for locale/class reasoning;
Branches
Unknown
Tags
Unknown