terru (Mar 18 2025 at 10:50): terru (Mar 18 2025 at 10:50):I'm aware of the "outline" document variant, which omits proofs. Is there also one which leave the structure of isar proofs, but omits only the proof methods (so have ?P by simp becomes something like have ?P <proof>)?
This would be useful for presenting the structure of a proof, without exposing the "machinery" of proof methods to readers who might be unfamiliar with Isabelle, for whom these are just visual clutter.
Last updated: Apr 03 2025 at 20:22 UTC