src/HOL/Auth/Message.ML

--- a/src/HOL/Auth/Message.ML	Thu Jul 08 13:37:40 1999 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Jul 08 13:38:41 1999 +0200
@@ -906,7 +906,7 @@
 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,