# HG changeset patch
# User wenzelm
# Date 1418150380 -3600
# Node ID c90c029409649ffe0845fd3a95bbb4b066cc0541
# Parent  fe7f91f85789d4689abfef3ae0d3d2e193a1d079
tuned spelling;

diff -r fe7f91f85789 -r c90c02940964 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
 *)