src/Tools/eqsubst.ML

   (* tactics *)
   val eqsubst_asm_tac: Proof.context -> int list -> thm list -> int -> tactic
   val eqsubst_asm_tac': Proof.context ->
     (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic
   val eqsubst_tac: Proof.context ->
-    int list -> (* list of occurences to rewrite, use [0] for any *)
+    int list -> (* list of occurrences to rewrite, use [0] for any *)
     thm list -> int -> tactic
   val eqsubst_tac': Proof.context ->
     (searchinfo -> term -> match Seq.seq) (* search function *)
     -> thm (* equation theorem to rewrite with *)
     -> int (* subgoal number in goal theorem *)

         |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r)
       end;
   in stepthms |> Seq.maps rewrite_with_thm end;
 
 
-(* General substitution of multiple occurances using one of
+(* General substitution of multiple occurrences using one of
    the given theorems *)
 
 fun skip_first_occs_search occ srchf sinfo lhs =
   (case skipto_skipseq occ (srchf sinfo lhs) of
     SkipMore _ => Seq.empty
   | SkipSeq ss => Seq.flat ss);
 
-(* The "occs" argument is a list of integers indicating which occurence
+(* The "occs" argument is a list of integers indicating which occurrence
 w.r.t. the search order, to rewrite. Backtracking will also find later
-occurences, but all earlier ones are skipped. Thus you can use [0] to
+occurrences, but all earlier ones are skipped. Thus you can use [0] to
 just find all rewrites. *)
 
 fun eqsubst_tac ctxt occs thms i st =
   let val nprems = Thm.nprems_of st in
     if nprems < i then Seq.empty else