--- a/src/HOL/BNF/More_BNFs.thy Sat Jul 06 22:16:55 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Fri Jul 05 18:10:07 2013 +0200
@@ -391,7 +391,7 @@
next
case False
hence "|{X. X \<subseteq> A \<and> countable X}| =o |{X. X \<subseteq> A \<and> countable X} - {{}}|"
- by (intro card_of_infinite_diff_finitte finite.emptyI finite.insertI ordIso_symmetric)
+ by (intro card_of_infinite_diff_finite finite.emptyI finite.insertI ordIso_symmetric)
(unfold finite_countable_subset)
also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Sat Jul 06 22:16:55 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Jul 05 18:10:07 2013 +0200
@@ -997,7 +997,7 @@
lemma infinite_card_of_diff_singl:
assumes "infinite A"
shows "|A - {a}| =o |A|"
-by (metis assms card_of_infinite_diff_finitte finite.emptyI finite_insert)
+by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
lemma card_of_vimage:
assumes "B \<subseteq> range f"
@@ -1066,7 +1066,7 @@
moreover
{have 2: "infinite (Bpow r A)" using infinite_Bpow[OF rc r A] .
have "|Bpow r A| =o |Bpow r A - {{}}|"
- using card_of_infinite_diff_finitte
+ using card_of_infinite_diff_finite
by (metis Pow_empty 2 finite_Pow_iff infinite_imp_nonempty ordIso_symmetric)
}
ultimately show ?thesis by (metis ordIso_ordLeq_trans)
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy Sat Jul 06 22:16:55 2013 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy Fri Jul 05 18:10:07 2013 +0200
@@ -2199,8 +2199,7 @@
subsection {* Others *}
-(* FIXME: finitte ~> finite? *)
-lemma card_of_infinite_diff_finitte:
+lemma card_of_infinite_diff_finite:
assumes "infinite A" and "finite B"
shows "|A - B| =o |A|"
by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
@@ -2294,8 +2293,7 @@
qed
qed
-(* FIXME: betwe ~> betw? *)
-lemma bij_betwe_curr:
+lemma bij_betw_curr:
"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
unfolding bij_betw_def inj_on_def image_def
using curr_in curr_inj curr_surj by blast
@@ -2303,7 +2301,7 @@
lemma card_of_Func_Times:
"|Func (A <*> B) C| =o |Func A (Func B C)|"
unfolding card_of_ordIso[symmetric]
-using bij_betwe_curr by blast
+using bij_betw_curr by blast
definition Func_map where
"Func_map B2 f1 f2 g b2 \<equiv>