doc(tactic/lean_core_docs): by_cases is classical (#3718)

`by_cases` was changed to use classical reasoning (#3354, leanprover-community/lean#409), but the documentation hasn't been updated yet.

I leave `by_contra` alone as it still uses `decidable`.

src/tactic/lean_core_docs.lean

@@ -110,10 +110,7 @@ add_tactic_doc
 `h : ¬ p` in the second branch. You can specify the name of the new hypothesis using the syntax
 `by_cases h : p`.
 
-This tactic requires that `p` is decidable. To ensure that all propositions are decidable via
-classical reasoning, use `open_locale classical`
-(or `local attribute [instance, priority 10] classical.prop_decidable` if you are not using
-mathlib).
+If `p` is not already decidable, `by_cases` will use the instance `classical.prop_decidable p`.
 -/
 add_tactic_doc
 { name       := "by_cases",