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