Classical.not_forall

Stream: std4

[Scott Morrison]

When I moved not_forall up to Std, I put it in the Classical namespace, since that's how Std seems to do things. Was that correct?

On that assumption, as I do the Mathlib bump I am adjusting for this change. Please let me know if instead I should change Std to pull it out of the namespace.

[Mario Carneiro]

yup, std puts all of those lemmas in the classical namespace and mathlib is responsible for aliasing or re-exporting them to the root namespace

[Scott Morrison]

#7724