src/Provers/classical.ML

--- a/src/Provers/classical.ML	Tue Dec 09 19:01:07 2014 +0100
+++ b/src/Provers/classical.ML	Tue Dec 09 19:39:40 2014 +0100
@@ -139,7 +139,7 @@
     [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
 
 Such rules can cause fast_tac to fail and blast_tac to report "PROOF
-FAILED"; classical_rule will strenthen this to
+FAILED"; classical_rule will strengthen this to
 
     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
 *)