Deprecate and remove `inductive` ... `:=`

Description

Today, Lean accepts all of the following:

inductive DogSound
  | woof
  | grr

inductive DogSound :=
  | woof
  | grr

inductive DogSound where
  | woof
  | grr

It seems that the overwhelming majority of declarations use the latter syntax (with where). In the interest of simplifying things, how about we deprecate the first two?

Context

The broad context here is that I'm writing the new reference manual with tooling that can let us know about undocumented tokens. The documentation should be comprehensive and describe what the language does.

Deprecating these two alternate syntaxes, rather than documenting them, would make Lean code more uniform and reduce the language surface area.

I'm not advocating immediate removal - a long deprecation period won't hurt anything - but a warning would be useful.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Read the three syntax examples and determine how the first two should be distinguished from the where form. Done means Lean warns on the inductive forms using ... and :=, while continuing to accept the where syntax; the issue does not name implementation files or tests.