Factorization

--- a/NEWS	Thu Mar 09 14:19:15 2000 +0100
+++ b/NEWS	Thu Mar 09 16:07:01 2000 +0100
@@ -50,6 +50,8 @@
 * HOL/record: fixed select-update simplification procedure to handle
 extended records as well; admit "r" as field name;
 
+* HOL/ex: new theory Factorization proving the Fundamental Theorem of
+Arithmetic, by Thomas M Rasmussen;
 
 *** General ***