From 9aac1a22c4ff4b4be16800b86e34a94d358b0deb Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 16 Jul 2025 12:36:32 +0200
Subject: Add quantified calcs and relax tokenization

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.
---
 source/Api.hs | 1 -
 1 file changed, 1 deletion(-)

(limited to 'source/Api.hs')

diff --git a/source/Api.hs b/source/Api.hs
index 1bdf615..866115d 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -67,7 +67,6 @@ import Text.Megaparsec hiding (parse, Token)
 import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment
-import Syntax.Abstract (Formula)
 
 -- | Follow all @\\import@ statements recursively and build a theory graph from them.
 -- The @\\import@ statements should be on their own separate line and precede all
-- 
cgit v1.2.3