summaryrefslogtreecommitdiff
path: root/library/ordinal.tex
AgeCommit message (Collapse)Author
2025-07-16Add quantified calcs and relax tokenizationadelon
Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.
2025-07-08Update lemma nameadelon
2024-07-02Further Formalisation of naturals.Simon-Kor
Such as induction on naturals and addition laws.
2024-02-10Initial commitadelon