--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Wed Jan 22 09:45:30 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Wed Jan 22 10:13:40 2014 +0100
@@ -5,7 +5,7 @@
Cardinal arithmetic.
*)
-header {* Cardinal Arithmetic *}
+header {* Cardinal Arithmetic *}
theory Cardinal_Arithmetic
imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
@@ -201,7 +201,6 @@
"\<lbrakk>Cinfinite r; |I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r\<rbrakk> \<Longrightarrow> |SIGMA i : I. A i| \<le>o r"
unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field)
-
lemma card_order_cexp:
assumes "card_order r1" "card_order r2"
shows "card_order (r1 ^c r2)"