Email Gateway (May 26 2025 at 13:20): Email Gateway (May 26 2025 at 13:20):From: i n <cl-isabelle-users@lists.cam.ac.uk>
Hi list,
Is there any reason why declare [[blast_trace]] and supply [[blast_trace]] is not made to work? I understand that I can do
ML‹Context.>> (Context.map_theory (Config.put_global Blast.trace (true)))›
```and
```ML_prf‹Context.>> (Context.map_proof (Config.put Blast.trace (true)))›```
but that's much more to type.
Thanks,
Irvin
Last updated: May 30 2025 at 04:27 UTC