--- a/NEWS Fri Sep 15 15:30:50 2000 +0200
+++ b/NEWS Fri Sep 15 15:48:41 2000 +0200
@@ -31,7 +31,7 @@
f.simps instead of f.rules;
* HOL: theory Sexp now in HOL/Induct examples (it used to be part of
-main HOL, but was unused); should better use HOL's datatype package
+main HOL, but was unused); it is better to use HOL's datatype package
anyway;
* HOL: removed obsolete theorem binding expand_if (refer to split_if
@@ -39,6 +39,16 @@
* HOL: less_induct is renamed nat_less_induct
+* HOL: systematic renaming of the @-rules:
+ selectI -> someI
+ selectI2 -> someI2
+ selectI2EX -> someI2_ex
+ select_equality -> some_equality
+ select1_equality -> some1_equality
+ select_eq_Ex -> some_eq_ex
+ Eps_eq -> some_eq_trivial
+ Eps_sym_eq -> some_sym_eq_trivial
+
* HOL/Real: "rabs" replaced by overloaded "abs" function;
* HOL/ML: even fewer consts are declared as global (see theories Ord,
--- a/TFL/thms.sml Fri Sep 15 15:30:50 2000 +0200
+++ b/TFL/thms.sml Fri Sep 15 15:48:41 2000 +0200
@@ -22,7 +22,7 @@
val CUT_DEF = get_thm WF.thy "cut_def";
val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
- (fn _ => [strip_tac 1, rtac selectI 1, assume_tac 1]);
+ (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);