Adam Dingle (Mar 21 2026 at 11:42): Adam Dingle (Mar 21 2026 at 11:42):In either jEdit or VS Code, is there some way to show the assumptions that are active at any point in a proof, along with their names?
For example, suppose that I'm proving P(n) by induction over the natural numbers. My proof will have cases "case 0" and "case (Suc n)". I know from the Programming and Proving tutorial that "case (Suc n)" will automatically introduce an assumption "P(n)" with name Suc. But that's not very evident from the user interface. If I click on the case statement itself, the proof state shows "this: P(n)", but it doesn't reveal that the assumption is named "Suc". Furthermore, if I click on any line following the "case" statement then the assumption is not displayed. I would expect the proof state to show me all the assumptions that are in scope at any given point, along with their names. Is that simply not how it works?
Alex Mobius (Mar 21 2026 at 16:52):print_facts, see Isar reference section 3.4 for more commands. Idk if you can make jEdit to show this at all times.
Last updated: Mar 25 2026 at 02:29 UTC