Closed yutakang closed 4 years ago
This makes it impossible to do Deep-Dive.
This is solved by transforming Proof.context.
Proof_Context.set_mode (Proof_Context.mode_abbrev ctxt)
This makes it impossible to do Deep-Dive.