NEWS
changeset 8392 5bf82327aa36
parent 8358 a57d72b5d272
child 8412 65f9089f6f71
     1.1 --- a/NEWS	Thu Mar 09 14:19:15 2000 +0100
     1.2 +++ b/NEWS	Thu Mar 09 16:07:01 2000 +0100
     1.3 @@ -50,6 +50,8 @@
     1.4  * HOL/record: fixed select-update simplification procedure to handle
     1.5  extended records as well; admit "r" as field name;
     1.6  
     1.7 +* HOL/ex: new theory Factorization proving the Fundamental Theorem of
     1.8 +Arithmetic, by Thomas M Rasmussen;
     1.9  
    1.10  *** General ***
    1.11