Commit 2026-06-04 02:30 6da04919
View on Github →feat(ModelTheory/Semantics): add simp theorems similar to Sentence.realize_not (#39996) Add simp theorems Sentence.realize_bot, Sentence.realize_top, Sentence.realize_inf, Sentence.realize_sup, Sentence.realize_imp and Sentence.realize_iff in the style of Sentence.realize_not as consequences of the corresponding theorems for formulas.