NEWS
changeset 12924 02eb40cde931
parent 12917 0fd3caa5d8b2
child 12964 2ac9265b2cd5
     1.1 --- a/NEWS	Thu Feb 21 20:11:05 2002 +0100
     1.2 +++ b/NEWS	Thu Feb 21 20:11:32 2002 +0100
     1.3 @@ -261,6 +261,9 @@
     1.4  
     1.5  * HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
     1.6  
     1.7 +* HOL: removed obsolete theorem "optionE" (use "option.exhaust", or
     1.8 +the "cases" method);
     1.9 +
    1.10  * HOL/GroupTheory: group theory examples including Sylow's theorem (by
    1.11  Florian Kammüller);
    1.12