* HOL: removed obsolete theorem "optionE";
authorwenzelm
Thu Feb 21 20:11:32 2002 +0100 (2002-02-21)
changeset 1292402eb40cde931
parent 12923 9ba7c5358fa0
child 12925 99131847fb93
* HOL: removed obsolete theorem "optionE";
NEWS
     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