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