HomePhabricator

more robust Thm.expose_theory -- ensure that PIDE export happens in the proper…

Authored by makarius.

Description

more robust Thm.expose_theory -- ensure that PIDE export happens in the proper theory context;

Details