diff -r 073f041d83ae -r 8bee5ca99e63 src/HOL/Cardinals/README.txt
--- a/src/HOL/Cardinals/README.txt	Mon Nov 18 18:04:44 2013 +0100
+++ b/src/HOL/Cardinals/README.txt	Mon Nov 18 18:04:44 2013 +0100
@@ -90,8 +90,8 @@
 ---------------------------------------
 
 1. Most of the definitions and theorems are proved in files suffixed with
-"_Base". Bootstrapping considerations (for the (co)datatype package) made this
-division desirable.
+"_LFP" or "_GFP". Bootstrapping considerations (for the (co)datatype package) made
+this division desirable.
 
 
 2. Even though we would have preferred to use "initial segment" instead of 
@@ -148,7 +148,7 @@
 Notes for anyone who would like to enrich these theories in the future
 --------------------------------------------------------------------------------------
 
-Theory Fun_More (and Fun_More_Base):
+Theory Fun_More (and Fun_More_*):
 - Careful: "inj" is an abbreviation for "inj_on UNIV", while  
   "bij" is not an abreviation for "bij_betw UNIV UNIV", but 
   a defined constant; there is no "surj_betw", but only "surj". 
@@ -166,7 +166,7 @@
 - In subsection "Other facts": 
 -- Does the lemma "atLeastLessThan_injective" already exist anywhere? 
 
-Theory Order_Relation_More (and Order_Relation_More_Base):
+Theory Order_Relation_More (and Order_Relation_More_*):
 - In subsection "Auxiliaries": 
 -- Recall the lemmas "order_on_defs", "Field_def", "Domain_def", "Range_def", "converse_def". 
 -- Recall that "refl_on r A" forces r to not be defined outside A.  
@@ -181,16 +181,16 @@
    abbreviation "Linear_order r ≡ linear_order_on (Field r) r"
    abbreviation "Well_order r ≡ well_order_on (Field r) r"
 
-Theory Wellorder_Relation (and Wellorder_Relation_Base):
+Theory Wellorder_Relation (and Wellorder_Relation_*):
 - In subsection "Auxiliaries": recall lemmas "order_on_defs"
 - In subsection "The notions of maximum, minimum, supremum, successor and order filter": 
   Should we define all constants from "wo_rel" in "rel" instead, 
   so that their outside definition not be conditional in "wo_rel r"? 
 
-Theory Wellfounded_More (and Wellfounded_More_Base):
+Theory Wellfounded_More (and Wellfounded_More_*):
   Recall the lemmas "wfrec" and "wf_induct". 
 
-Theory Wellorder_Embedding (and Wellorder_Embedding_Base):
+Theory Wellorder_Embedding (and Wellorder_Embedding_*):
 - Recall "inj_on_def" and "bij_betw_def". 
 - Line 5 in the proof of lemma embed_in_Field: we have to figure out for this and many other 
   situations:  Why did it work without annotations to Refl_under_in?
@@ -200,7 +200,7 @@
   making impossible to debug theorem instantiations.  
 - At lemma "embed_unique": If we add the attribute "rule format" at lemma, we get an error at qed.
 
-Theory Constructions_on_Wellorders (and Constructions_on_Wellorders_Base):
+Theory Constructions_on_Wellorders (and Constructions_on_Wellorders_*):
 - Some of the lemmas in this section are about more general kinds of relations than 
   well-orders, but it is not clear whether they are useful in such more general contexts.
 - Recall that "equiv" does not have the "equiv_on" and "Equiv" versions, 
@@ -208,7 +208,7 @@
 - The lemmas "ord_trans" are not clearly useful together, as their employment within blast or auto 
 tends to diverge.  
 
-Theory Cardinal_Order_Relation (and Cardinal_Order_Relation_Base):
+Theory Cardinal_Order_Relation (and Cardinal_Order_Relation_*):
 - Careful: if "|..|" meets an outer parehthesis, an extra space needs to be inserted, as in
   "( |A| )". 
 - At lemma like ordLeq_Sigma_mono1: Not worth stating something like ordLeq_Sigma_mono2 --