*** empty log message ***

--- 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);