src/HOL/Auth/Message.ML

 
 (** Useful in many uniqueness proofs **)
 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
                      assume_tac (i+1);
 
-(*Apply the EX-ALL quantifification to prove uniqueness theorems in 
+(*Apply the EX-ALL quantification to prove uniqueness theorems in 
   their standard form*)
 fun prove_unique_tac lemma = 
   EVERY' [dtac lemma,
           REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
           (*Duplicate the assumption*)