Commit 2022-11-07 21:34 c11114aa

feat: classical tactic (#540) Note that classical had to be turned into a scoping tactic, because AFAIK there isn't a way to perform additional actions at the end of elaboration. In lean 3 this wasn't a problem since the environment is rolled back after a theorem is elaborated, but in lean 4 you can add global definitions during elaboration of a theorem so something has to clean up afterward.