src/Provers/blast.ML

 
 Known problems:
   "Recursive" chains of rules can sometimes exclude other unsafe formulae
 	from expansion.  This happens because newly-created formulae always
 	have priority over existing ones.  But obviously recursive rules 
-	such as transitivity are treated specially to prevent this.  SOMEtimes
+	such as transitivity are treated specially to prevent this.  Sometimes
 	the formulae get into the wrong order (see WRONG below).
 
   With substition for equalities (hyp_subst_tac):
         When substitution affects a haz formula or literal, it is moved
         back to the list of safe formulae.