felix.git/library/set/regularity.tex, branch hotgUnnamed repository; edit this file 'description' to name the repository.
https://git.adelon.net/felix.git/atom?h=hotg2026-08-06T12:42:39+00:00Remove some ZF stuff2026-08-06T12:42:39+00:00adelon22380201+adelon@users.noreply.github.com2026-08-06T12:42:39+00:00urn:sha1:742bf9877c803da0aa89f6aa510bb20514dba56fRewrite protected set and naturals closure2026-08-02T16:42:54+00:00adelon22380201+adelon@users.noreply.github.com2026-08-02T16:42:54+00:00urn:sha1:5f64079c4ec671de04971f38907805e9de514537Make handling of local variables stricter2026-04-12T13:25:03+00:00adelon22380201+adelon@users.noreply.github.com2026-04-12T13:25:03+00:00urn:sha1:bb4497227eb1ab060311baf0664865979655e03cUpdate regularity.tex2025-12-03T00:01:06+00:00adelon22380201+adelon@users.noreply.github.com2025-12-03T00:01:06+00:00urn:sha1:94d3c5a6a4dd986394a22cc83c87d71c56e17874Add quantified calcs and relax tokenization2025-07-16T10:36:32+00:00adelon22380201+adelon@users.noreply.github.com2025-07-16T10:36:32+00:00urn: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.
Linting and optimization2025-07-08T19:20:20+00:00adelon22380201+adelon@users.noreply.github.com2025-07-08T19:20:20+00:00urn:sha1:51fe28bdd9943e359de5835d2737c0fdc8618df7Initial commit2024-02-10T01:22:14+00:00adelon22380201+adelon@users.noreply.github.com2024-02-10T01:22:14+00:00urn:sha1:442d732696ad431b84f6e5c72b6ee785be4fd968