From ebfd3b93e80e29ae1839492c1098233b210f55af Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Fri, 24 May 2024 12:02:29 -0500
Subject: [PATCH] Remove confusing sentence fragment
---
spec/doc.tex | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index 6f50f5d..be140d5 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -832,8 +832,7 @@ is always \inlineAlethe{Int}.
For example, in standard {\smtlib}, the term \inlineAlethe{(+ 5 3)}
has the sort \inlineAlethe{Int} in the logic \texttt{QF\_LIA}, but
has the sort \inlineAlethe{Real} in \texttt{QF\_LRA}.
-In Alethe, this term always has the sort \inlineAlethe{Int},
-and would not be well sorted in the logic \texttt{QF\_LRA}.
+In Alethe, this term always has the sort \inlineAlethe{Int}.
\paragraph{Subproofs}
The abstract notation denotes subproofs by marking them with a vertical
--
GitLab