Merge remote-tracking branch 'origin/main' into isabelle2020-dune

tlaplus · Dec 23, 2023 · 501564e · 501564e
2 parents 21bbf9f + a0ae986
commit 501564e
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/test/fast/regression/setEuclid_test.tla b/test/fast/regression/setEuclid_test.tla
@@ -361,7 +361,10 @@ THEOREM Inv /\ Next => Inv'
 (*|*)   BY <3>1, <3>2
     <2>3. CorrectTermination'
       <3>1. Cardinality (S) = 1 => S = {CHOOSE t \in S : TRUE}
-        BY CardThm DEF Inv, TypeOK
+        <4> Cardinality (S) = 1 => \E x \in S : S = {x}
+          BY CardThm DEF Inv, TypeOK
+        <4> QED
+          BY Zenon
       <3>2. Cardinality (S) = 1 => GCD (S) = CHOOSE t \in S : TRUE
         BY <3>1, GCD2 DEF Inv, TypeOK
       <3> QED