Adapt `classical` to new semantics

We've recently changed `classical` in mathlib to so that it no longer overrides the existing decidable instances.  mathlib4 should be adapterd.  https://github.com/leanprover-community/mathlib/pull/14122

```lean
import Mathlib.Tactic.Basic

example : (by classical; exact decide (0 = 1) : Bool) = decide (0 = 1) := rfl -- this should work
```