# HG changeset patch
# User wenzelm
# Date 1211061200 -7200
# Node ID 64e850c3da9ed895296b79d2471f61f5989761bf
# Parent  57e7d045774a3c0ae87f7fa95b75579bca373ccf
tuned comments;

diff -r 57e7d045774a -r 64e850c3da9e src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat May 17 23:53:19 2008 +0200
+++ b/src/Provers/blast.ML	Sat May 17 23:53:20 2008 +0200
@@ -587,7 +587,7 @@
 val dummyTVar = Term.TVar(("a",0), []);
 val dummyVar2 = Term.Var(("var",0), dummyT);
 
-(*convert Blast_tac's type representation to real types for tracing*)
+(*convert blast_tac's type representation to real types for tracing*)
 fun showType (Free a)  = Term.TFree (a,[])
   | showType (Var _)   = dummyTVar
   | showType t         =
diff -r 57e7d045774a -r 64e850c3da9e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat May 17 23:53:19 2008 +0200
+++ b/src/Provers/classical.ML	Sat May 17 23:53:20 2008 +0200
@@ -170,7 +170,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
+Such rules can cause fast_tac to fail and blast_tac to report "PROOF
 FAILED"; classical_rule will strenthen this to
 
     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W