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
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