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