Commit 2024-01-30 16:52 d5057d5c

View on Github →

chore: remove classical, it has been moved to Std (#10121)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Pi/Algebra.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Tactic.lean

Deleted Mathlib/Tactic/Classical.lean

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/Tauto.lean

Deleted test/classical.lean

deleted def bar''

deleted def bar'

deleted def bar