Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] blast_trace

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: Nov 09 2025 at 20:21 UTC