src/HOL/simpdata.ML

 val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover;
 
 end; (*local*)
 
 
-(* Simproc for Let *)
+(* simproc for Let *)
 
 val use_let_simproc = ref true;
 
 local
   val thy = the_context ();

         | _ => NONE)
      end)
 
 end; (*local*)
 
-(* A general refutation procedure *)
-
-(* Parameters:
+(* generic refutation procedure *)
+
+(* parameters:
 
    test: term -> bool
    tests if a term is at all relevant to the refutation proof;
    if not, then it can be discarded. Can improve performance,
    esp. if disjunctions can be discarded (no case distinction needed!).