# HG changeset patch
# User traytel
# Date 1373040607 -7200
# Node ID 0c4b140cff00533c475908e2ad52435ca4065e2f
# Parent  6f5678b97c4ecef3d78fd9987bda4b953a611983
tuned spelling

diff -r 6f5678b97c4e -r 0c4b140cff00 src/HOL/BNF/More_BNFs.thy
--- 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
diff -r 6f5678b97c4e -r 0c4b140cff00 src/HOL/Cardinals/Cardinal_Order_Relation.thy
--- 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)
diff -r 6f5678b97c4e -r 0c4b140cff00 src/HOL/Cardinals/Cardinal_Order_Relation_Base.thy
--- 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>