# HG changeset patch
# User wenzelm
# Date 967636932 -7200
# Node ID 0502f06c2d294e598e5f54e3ef954425572ce097
# Parent  1c5b0f27de569af9548d17a353dd96929499e39a
fixed name;

diff -r 1c5b0f27de56 -r 0502f06c2d29 NEWS
--- 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);