1.1 --- a/src/HOL/HOL_lemmas.ML	Fri Sep 15 20:20:45 2000 +0200
     1.2 +++ b/src/HOL/HOL_lemmas.ML	Fri Sep 15 20:22:00 2000 +0200
     1.3 @@ -373,7 +373,7 @@
     1.4  val [major,minor] = Goal "[| EX a. P a;  !!x. P x ==> Q x |] ==> Q (Eps P)";
     1.5  by (rtac (major RS exE) 1);
     1.6  by (etac someI2 1 THEN etac minor 1);
     1.7 -qed "someI2EX";
     1.8 +qed "someI2_ex";
     1.9  
    1.10  val prems = Goal
    1.11      "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";

     2.1 --- a/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 20:20:45 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 20:22:00 2000 +0200
     2.3 @@ -6,5 +6,5 @@
     2.4  
     2.5  Goalw [newref_def]
     2.6   "hp x = None \\<longrightarrow> hp (newref hp) = None";
     2.7 -by (fast_tac (claset() addIs [someI2EX] addss (simpset())) 1);
     2.8 +by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
     2.9  qed_spec_mp "newref_None";

     3.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 20:20:45 2000 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 20:22:00 2000 +0200
     3.3 @@ -97,7 +97,7 @@
     3.4    "[| is_normed_vectorspace V norm; is_continuous V norm f|]
     3.5       ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
     3.6  proof (unfold function_norm_def is_function_norm_def 
     3.7 -  is_continuous_def Sup_def, elim conjE, rule someI2EX)
     3.8 +  is_continuous_def Sup_def, elim conjE, rule someI2_ex)
     3.9    assume "is_normed_vectorspace V norm"
    3.10    assume "is_linearform V f" 
    3.11    and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"

     4.1 --- a/src/HOL/WF_Rel.ML	Fri Sep 15 20:20:45 2000 +0200
     4.2 +++ b/src/HOL/WF_Rel.ML	Fri Sep 15 20:22:00 2000 +0200
     4.3 @@ -150,14 +150,14 @@
     4.4   by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
     4.5   by (rtac allI 1);
     4.6   by (Simp_tac 1);
     4.7 - by (rtac someI2EX 1);
     4.8 + by (rtac someI2_ex 1);
     4.9    by (Blast_tac 1);
    4.10   by (Blast_tac 1);
    4.11  by (rtac allI 1);
    4.12  by (induct_tac "n" 1);
    4.13   by (Asm_simp_tac 1);
    4.14  by (Simp_tac 1);
    4.15 -by (rtac someI2EX 1);
    4.16 +by (rtac someI2_ex 1);
    4.17   by (Blast_tac 1);
    4.18  by (Blast_tac 1);
    4.19  qed "wf_iff_no_infinite_down_chain";