# HG changeset patch
# User wenzelm
# Date 968354298 -7200
# Node ID 7c7ff65b684683d9210a1587536eac0c1320a4b7
# Parent  473a6604da94ae9940f8f5bd92eced23e95b5dae
HOL: qed_spec_mp now also removes bounded ALL;
Isar: renamed some attributes;

diff -r 473a6604da94 -r 7c7ff65b6846 NEWS
--- a/NEWS	Thu Sep 07 21:12:49 2000 +0200
+++ b/NEWS	Thu Sep 07 21:18:18 2000 +0200
@@ -45,8 +45,10 @@
 Lfp, Gfp, WF); this only affects ML packages that refer to const names
 internally;
 
-* HOL, ZF: syntax for quotienting wrt an equivalence relation changed from
-  A/r to A//r;
+* HOL, ZF: syntax for quotienting wrt an equivalence relation changed
+from A/r to A//r;
+
+* HOL: qed_spec_mp now also removes bounded ALL;
 
 * ZF: new treatment of arithmetic (nat & int) may break some old proofs;
 
@@ -58,6 +60,8 @@
 
 * Isar: renamed 'RS' attribute to 'THEN';
 
+* Isar: renamed some attributes (rulify -> rulified, elimify -> elimified, ...);
+
 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
 
 * Provers: strengthened force_tac by using new first_best_tac;
@@ -293,8 +297,8 @@
 induct_tac th "x1 ... xn" expects th to have a conclusion of the form
 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th;
 
-* new function rulify: thm -> thm for turning outer -->/! into ==>/?;
-behaves like qed_spec_mp;
+* new functions rulify/rulify_no_asm: thm -> thm for turning outer
+-->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm;
 
 * theory Sexp now in HOL/Induct examples (it used to be part of main
 HOL, but was unused);