In my current (apply script) proof I am using the subgoal command to focus on premises and parameters. But after solving the subgoal, when I use `done`

I get an Option error in basics.ML. I think I had this once where I unfolded `atomize_imp[symmetric]`

under the subgoal, but this time I am not doing that.

What could be the reason for this error? The proof is quite long and relies on other theorems so I can't really post it as reference

This is the error in jEdit (I have nested `subgoal`

): image.png

Ok, my hunch was right, changing my proof to not use `apply (unfold atomize_imp[symmetric] atomize_all[symmetric])`

fixes this issue

Last updated: Feb 27 2024 at 08:17 UTC