src/HOL/Cardinals/README.txt

      of cardinal and the numeric one previously defined for
      finite sets (operator "card").  On the way, one introduces the cardinal omega
      (natLeq) and the finite cardinals (natLeq_on n).
 ---- 6) Defines and proves the existence of successor cardinals.  
 
--- Cardinal_Arithmetic
+-- BNF_Cardinal_Arithmetic
 
 
 Here is a list of names of proved facts concerning cardinalities that are 
 expressed independently of notions of order, and of potential interest 
 for "working mathematicians":

 
 
 Minor technicalities and naming issues:
 ---------------------------------------
 
-1. Most of the definitions and theorems are proved in files suffixed with "_FP".
+1. Most of the definitions and theorems are proved in files prefixed with "BNF_".
 Bootstrapping considerations (for the (co)datatype package) made this division
 desirable.
 
 
 2. Even though we would have preferred to use "initial segment" instead of

    abbreviation "Partial_order r ≡ partial_order_on (Field r) r"
    abbreviation "Total r ≡ total_on (Field r) r"
    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_FP):
+Theory Wellorder_Relation (and BNF_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:
   Recall the lemmas "wfrec" and "wf_induct". 
 
-Theory Wellorder_Embedding (and Wellorder_Embedding_FP):
+Theory Wellorder_Embedding (and BNF_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?
 - At the proof of theorem "wellorders_totally_ordered" (and, similarly, elsewhere): 
   Had we used metavariables instead of local definitions for H, f, g and test, the 
   goals (in the goal window) would have become unreadable, 
   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_FP):
+Theory Constructions_on_Wellorders (and BNF_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, 
  like the order relation. "equiv" corresponds, for instance, to "well_order_on". 
 - 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_FP):
+Theory Cardinal_Order_Relation (and BNF_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 -- 
   would be a mere instance of card_of_Sigma_mono2.  
 - At lemma ordLeq_Sigma_cong2: Again, no reason for stating something like ordLeq_Sigma_cong2.