src/HOL/hologic.ML

   | dest_mem t = raise TERM ("dest_mem", [t]);
 
 fun mk_UNIV T = Const ("UNIV", mk_setT T);
 
 
-(* binary oprations and relations *)
+(* binary operations and relations *)
 
 fun mk_binop c (t, u) =
   let val T = fastype_of t in
     Const (c, [T, T] ---> T) $ t $ u
   end;

 
 (* binary numerals *)
 
 val binT = Type ("Numeral.bin", []);
 
-val pls_const =  Const ("Numeral.bin.Pls", binT)
+val pls_const = Const ("Numeral.bin.Pls", binT)
 and min_const = Const ("Numeral.bin.Min", binT)
 and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
 
 fun number_of_const T = Const ("Numeral.number_of", binT --> T);