# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 6207fd64519bdf3d6a77ac095bdcd319ec28da43
# Parent  6d3fad6f01c98fcdcb5628d81e0dc5d4ab3102a7
tuned comment

diff -r 6d3fad6f01c9 -r 6207fd64519b src/HOL/Cardinals/README.txt
--- a/src/HOL/Cardinals/README.txt	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/README.txt	Mon Jan 20 18:24:56 2014 +0100
@@ -67,7 +67,9 @@
      (natLeq) and the finite cardinals (natLeq_on n).
 ---- 6) Defines and proves the existence of successor cardinals.  
 
--- BNF_Cardinal_Arithmetic
+Theory Ordinal_Arithmetic
+
+Theory Cardinal_Arithmetic (and BNF_Cardinal_Arithmetic)
 
 
 Here is a list of names of proved facts concerning cardinalities that are