wenzelm [Sat, 13 Dec 2008 15:06:24 +0100] rev 29093
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories;
added display_names -- user-level presentation;
removed obsolete exists_name, names_of;
tuned;