src/HOL/Hoare/hoare.ML

 end;
 
 
 (*****************************************************************************)
 (** Simplifying:                                                            **)
-(** Some useful lemmata, lists and simplification tactics to control which  **)
+(** SOME useful lemmata, lists and simplification tactics to control which  **)
 (** theorems are used to simplify at each moment, so that the original      **)
 (** input does not suffer any unexpected transformation                     **)
 (*****************************************************************************)
 
 Goal "-(Collect b) = {x. ~(b x)}";