# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1673732528 0
# Node ID f552cf789a8dc574d8b632c779f6d5da5493873e
# Parent  293caf3dbecd33fa9846de200e0cc2e37a9e55da
Missing theorem restored

diff -r 293caf3dbecd -r f552cf789a8d src/HOL/BNF_Cardinal_Arithmetic.thy
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Sat Jan 14 16:53:54 2023 +0000
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Sat Jan 14 21:42:08 2023 +0000
@@ -172,6 +172,10 @@
 lemma Cinfinite_csum1: "Cinfinite r1 \<Longrightarrow> Cinfinite (r1 +c r2)"
   by (blast intro!: Cinfinite_csum elim: )
 
+lemma Cinfinite_csum_weak:
+  "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
+by (erule Cinfinite_csum1)
+
 lemma csum_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 +c p2 =o r1 +c r2"
   by (simp only: csum_def ordIso_Plus_cong)