NEWS
changeset 9741 0502f06c2d29
parent 9737 7aae235675dc
child 9746 64b803edef39
--- a/NEWS	Wed Aug 30 13:55:26 2000 +0200
+++ b/NEWS	Wed Aug 30 14:02:12 2000 +0200
@@ -281,8 +281,8 @@
 
 * HOL: theorems impI, allI, ballI bound as "strip";
 
-* new function rulify: thm -> thm for turning outer -->/! into ==>/?; behaves
-like eq_spec_mp;
+* new function rulify: thm -> thm for turning outer -->/! into ==>/?;
+behaves like qed_spec_mp;
 
 * theory Sexp now in HOL/Induct examples (it used to be part of main
 HOL, but was unused);