classical tactic

def Lean.Elab.Tactic.classical {m : Type → Type} {α : Type} [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : m α) : m α

classical t runs t in a scope where Classical.propDecidable is a low priority local instance.

def Lean.Elab.Tactic.evalClassical : Tactic