Email Gateway (Aug 23 2022 at 08:31): Email Gateway (Aug 23 2022 at 08:31):From: Makarius <makarius@sketis.net>
Display in which situation? Do you mean the standard proof state output?
Checking the sources for that it turns out that it is indeed hardwired:
https://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2019/src/Pure/goal_display.ML#l113
Makarius
Email Gateway (Aug 23 2022 at 08:31):From: Joshua Chen <josh@joshchen.io>
Yes, I do mean in the standard proof state output. I thought so, thanks
for confirming!
Josh
Email Gateway (Aug 23 2022 at 08:33):From: Lawrence Paulson <lp15@cam.ac.uk>
Unfortunately not. And simply to hide them would make the output misleading. If you are getting them a lot, you are perhaps doing something unusual.
At the ML level, they can be eliminated by brute force using the tactic flexflex_tac, but this can lose information, and there is no corresponding Isar proof method.
Larry Paulson
Email Gateway (Aug 23 2022 at 08:47):From: Joshua Chen <josh@joshchen.io>
Dear list, is there a way to hide the display of flex-flex pairs?
Last updated: Apr 19 2024 at 12:27 UTC