tuned comments;
authorwenzelm
Sat May 17 23:53:20 2008 +0200 (2008-05-17)
changeset 2693864e850c3da9e
parent 26937 57e7d045774a
child 26939 1035c89b4c02
tuned comments;
src/Provers/blast.ML
src/Provers/classical.ML
     1.1 --- a/src/Provers/blast.ML	Sat May 17 23:53:19 2008 +0200
     1.2 +++ b/src/Provers/blast.ML	Sat May 17 23:53:20 2008 +0200
     1.3 @@ -587,7 +587,7 @@
     1.4  val dummyTVar = Term.TVar(("a",0), []);
     1.5  val dummyVar2 = Term.Var(("var",0), dummyT);
     1.6  
     1.7 -(*convert Blast_tac's type representation to real types for tracing*)
     1.8 +(*convert blast_tac's type representation to real types for tracing*)
     1.9  fun showType (Free a)  = Term.TFree (a,[])
    1.10    | showType (Var _)   = dummyTVar
    1.11    | showType t         =
     2.1 --- a/src/Provers/classical.ML	Sat May 17 23:53:19 2008 +0200
     2.2 +++ b/src/Provers/classical.ML	Sat May 17 23:53:20 2008 +0200
     2.3 @@ -170,7 +170,7 @@
     2.4  
     2.5      [| inj f; f x = f y; x = y ==> PROP W |] ==> PROP W
     2.6  
     2.7 -Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF
     2.8 +Such rules can cause fast_tac to fail and blast_tac to report "PROOF
     2.9  FAILED"; classical_rule will strenthen this to
    2.10  
    2.11      [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W