felix.git/library/ordinal.tex, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2026-08-03T16:21:05+00:00 Tighten ordinal premise selection 2026-08-03T16:21:05+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-03T16:13:54+00:00 urn:sha1:89a5acbcdf1f646ccb94a3f3c06a3d3824699de1 Migrate ordinal development 2026-08-03T16:00:08+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-03T16:00:08+00:00 urn:sha1:98d0a5c4a8949e31237d3c36564dbe1b4f5087ba Add quantified calcs and relax tokenization 2025-07-16T10:36:32+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-07-16T10:36:32+00:00 urn:sha1:9aac1a22c4ff4b4be16800b86e34a94d358b0deb 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. Update lemma name 2025-07-08T20:16:01+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-07-08T20:16:01+00:00 urn:sha1:da6d425281534407a92ce18a22584905a7847a39 Further Formalisation of naturals. 2024-07-02T19:24:44+00:00 Simon-Kor 52245124+Simon-Kor@users.noreply.github.com 2024-07-02T19:24:44+00:00 urn:sha1:bff76c7fabb9f2c0b9dcac915dfa68e930baf4d4 Such as induction on naturals and addition laws. Initial commit 2024-02-10T01:22:14+00:00 adelon 22380201+adelon@users.noreply.github.com 2024-02-10T01:22:14+00:00 urn:sha1:442d732696ad431b84f6e5c72b6ee785be4fd968