diff --git a/Std.lean b/Std.lean
index a866ba703d..9901959ed0 100644
--- a/Std.lean
+++ b/Std.lean
@@ -122,6 +122,7 @@ import Std.Tactic.Basic
 import Std.Tactic.ByCases
 import Std.Tactic.Case
 import Std.Tactic.Change
+import Std.Tactic.Classical
 import Std.Tactic.CoeExt
 import Std.Tactic.Congr
 import Std.Tactic.Exact
diff --git a/Std/Tactic/Classical.lean b/Std/Tactic/Classical.lean
new file mode 100644
index 0000000000..3bd386c858
--- /dev/null
+++ b/Std/Tactic/Classical.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Elab.ElabRules
+
+/-! # `classical` and `classical!` tactics -/
+
+namespace Std.Tactic
+open Lean Meta
+
+/--
+`classical!` adds a proof of `Classical.propDecidable` as a local variable, which makes it
+available for instance search and effectively makes all propositions decidable.
+```
+noncomputable def foo : Bool := by
+  classical!
+  have := ∀ p, decide p -- uses the classical instance
+  exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable
+```
+Consider using `classical` instead if you want to use the decidable instance when available.
+-/
+macro (name := classical!) "classical!" : tactic =>
+  `(tactic| have em := Classical.propDecidable)
+
+/--
+`classical tacs` runs `tacs` in a scope where `Classical.propDecidable` is a low priority
+local instance. It differs from `classical!` in that `classical!` uses a local variable,
+which has high priority:
+```
+noncomputable def foo : Bool := by
+  classical!
+  have := ∀ p, decide p -- uses the classical instance
+  exact decide (0 < 1) -- uses the classical instance even though `0 < 1` is decidable
+
+def bar : Bool := by
+  classical
+  have := ∀ p, decide p -- uses the classical instance
+  exact decide (0 < 1) -- uses the decidable instance
+```
+Note that (unlike lean 3) `classical` is a scoping tactic - it adds the instance only within the
+scope of the tactic.
+-/
+-- FIXME: using ppDedent looks good in the common case, but produces the incorrect result when
+-- the `classical` does not scope over the rest of the block.
+elab "classical" tacs:ppDedent(tacticSeq) : tactic => do
+  modifyEnv Meta.instanceExtension.pushScope
+  Meta.addInstance ``Classical.propDecidable .local 10
+  try Elab.Tactic.evalTactic tacs
+  finally modifyEnv Meta.instanceExtension.popScope
diff --git a/test/classical.lean b/test/classical.lean
new file mode 100644
index 0000000000..a9c527eb75
--- /dev/null
+++ b/test/classical.lean
@@ -0,0 +1,32 @@
+import Std.Tactic.Classical
+import Std.Tactic.PermuteGoals
+import Std.Tactic.GuardExpr
+
+noncomputable example : Bool := by
+  fail_if_success have := ∀ p, decide p -- no classical in scope
+  classical!
+  have := ∀ p, decide p -- uses the classical instance
+  -- uses the classical instance even though `0 < 1` is decidable
+  guard_expr decide (0 < 1) = @decide (0 < 1) (‹(a : Prop) → Decidable a› _)
+  exact decide (0 < 1)
+
+example : Bool := by
+  fail_if_success have := ∀ p, decide p -- no classical in scope
+  classical
+  have := ∀ p, decide p -- uses the classical instance
+  guard_expr decide (0 < 1) = @decide (0 < 1) (Nat.decLt 0 1)
+  exact decide (0 < 1) -- uses the decidable instance
+
+-- double check no leakage
+example : Bool := by
+  fail_if_success have := ∀ p, decide p -- no classical in scope
+  exact decide (0 < 1) -- uses the decidable instance
+
+-- check that classical respects tactic blocks
+example : Bool := by
+  fail_if_success have := ∀ p, decide p -- no classical in scope
+  on_goal 1 =>
+    classical
+    have := ∀ p, decide p -- uses the classical instance
+  fail_if_success have := ∀ p, decide p -- no classical in scope again
+  exact decide (0 < 1) -- uses the decidable instance