NEWS
changeset 5046 de5eacb7361a
parent 5044 59808d00ea8d
child 5047 585fa380df1a
--- a/NEWS	Thu Jun 18 10:48:21 1998 +0200
+++ b/NEWS	Thu Jun 18 10:50:16 1998 +0200
@@ -37,7 +37,7 @@
 * inductive definitions now handle disjunctive premises correctly (HOL
 and ZF);
 
-* new toplevel commands 'thm' and 'thms' for retrieving theorems from
+* new toplevel commands 'Thm' and 'Thms' for retrieving theorems from
 the current theory context;
 
 * new theory section 'nonterminals';