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