# HG changeset patch
# User nipkow
# Date 967634530 -7200
# Node ID 7aae235675dc1abaf9fd45c85f99a57f7b323c77
# Parent  332fab43628f5569c157c809f387c9cde9b67943
*** empty log message ***

diff -r 332fab43628f -r 7aae235675dc NEWS
--- a/NEWS	Wed Aug 30 10:21:19 2000 +0200
+++ b/NEWS	Wed Aug 30 13:22:10 2000 +0200
@@ -281,6 +281,9 @@
 
 * HOL: theorems impI, allI, ballI bound as "strip";
 
+* new function rulify: thm -> thm for turning outer -->/! into ==>/?; behaves
+like eq_spec_mp;
+
 * theory Sexp now in HOL/Induct examples (it used to be part of main
 HOL, but was unused);