HomePhabricator

uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with…

Authored by makarius.

Description

uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes;

Details

Committed
makariusNov 4 2019, 4:56 PM
Parents
rISABELLEb697dd74221a: tuned;
Branches
Unknown
Tags
Unknown