# HG changeset patch
# User Andreas Lochbihler
# Date 1428498160 -7200
# Node ID e936c2828bec86ae789cbc0246ce5f6b3956ddc1
# Parent  0145010f3f83ef99129fba7955dd7f2b46d441ff
consistent naming

diff -r 0145010f3f83 -r e936c2828bec src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Wed Apr 08 14:59:09 2015 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy	Wed Apr 08 15:02:40 2015 +0200
@@ -287,10 +287,10 @@
 lemmas cUn_cinsert_left[simp] = Un_insert_left[Transfer.transferred]
 lemmas cUn_cinsert_right[simp] = Un_insert_right[Transfer.transferred]
 lemmas cInt_cinsert_left = Int_insert_left[Transfer.transferred]
-lemmas cInt_cinsert_left_ifffempty[simp] = Int_insert_left_if0[Transfer.transferred]
+lemmas cInt_cinsert_left_if0[simp] = Int_insert_left_if0[Transfer.transferred]
 lemmas cInt_cinsert_left_if1[simp] = Int_insert_left_if1[Transfer.transferred]
 lemmas cInt_cinsert_right = Int_insert_right[Transfer.transferred]
-lemmas cInt_cinsert_right_ifffempty[simp] = Int_insert_right_if0[Transfer.transferred]
+lemmas cInt_cinsert_right_if0[simp] = Int_insert_right_if0[Transfer.transferred]
 lemmas cInt_cinsert_right_if1[simp] = Int_insert_right_if1[Transfer.transferred]
 lemmas cUn_cInt_distrib = Un_Int_distrib[Transfer.transferred]
 lemmas cUn_cInt_distrib2 = Un_Int_distrib2[Transfer.transferred]
@@ -345,11 +345,11 @@
 
 subsection {* Additional lemmas*}
 
-subsubsection {* @{text femepty} *}
+subsubsection {* @{text cempty} *}
 
 lemma cemptyE [elim!]: "cin a cempty \<Longrightarrow> P" by simp
 
-subsubsection {* @{text finsert} *}
+subsubsection {* @{text cinsert} *}
 
 lemma countable_insert_iff: "countable (insert x A) \<longleftrightarrow> countable A"
 by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable)