# HG changeset patch
# User paulson
# Date 969025721 -7200
# Node ID e0164f01d55a30ec45a48d8b9e860b77bc64e7da
# Parent  dfe4747c8318110f715b9489f38747d74c24e936
renamed the select rules

diff -r dfe4747c8318 -r e0164f01d55a NEWS
--- 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,
diff -r dfe4747c8318 -r e0164f01d55a TFL/thms.sml
--- 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]);