Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned comment
authorblanchet
Mon, 20 Jan 2014 18:24:56 +0100
changeset 55063 6207fd64519b
parent 55062 6d3fad6f01c9
child 55064 8dd21c4b0501
tuned comment
src/HOL/Cardinals/README.txt file | annotate | diff | comparison | revisions 
--- 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
isabelle