src/Tools/eqsubst.ML
changeset 58318 f95754ca7082
parent 54742 7a86358a3c0b
child 58826 2ed2eaabe3df
     1.1 --- a/src/Tools/eqsubst.ML	Thu Sep 11 20:01:29 2014 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu Sep 11 21:11:03 2014 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    val eqsubst_asm_tac': Proof.context ->
     1.5      (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic
     1.6    val eqsubst_tac: Proof.context ->
     1.7 -    int list -> (* list of occurences to rewrite, use [0] for any *)
     1.8 +    int list -> (* list of occurrences to rewrite, use [0] for any *)
     1.9      thm list -> int -> tactic
    1.10    val eqsubst_tac': Proof.context ->
    1.11      (searchinfo -> term -> match Seq.seq) (* search function *)
    1.12 @@ -292,7 +292,7 @@
    1.13    in stepthms |> Seq.maps rewrite_with_thm end;
    1.14  
    1.15  
    1.16 -(* General substitution of multiple occurances using one of
    1.17 +(* General substitution of multiple occurrences using one of
    1.18     the given theorems *)
    1.19  
    1.20  fun skip_first_occs_search occ srchf sinfo lhs =
    1.21 @@ -300,9 +300,9 @@
    1.22      SkipMore _ => Seq.empty
    1.23    | SkipSeq ss => Seq.flat ss);
    1.24  
    1.25 -(* The "occs" argument is a list of integers indicating which occurence
    1.26 +(* The "occs" argument is a list of integers indicating which occurrence
    1.27  w.r.t. the search order, to rewrite. Backtracking will also find later
    1.28 -occurences, but all earlier ones are skipped. Thus you can use [0] to
    1.29 +occurrences, but all earlier ones are skipped. Thus you can use [0] to
    1.30  just find all rewrites. *)
    1.31  
    1.32  fun eqsubst_tac ctxt occs thms i st =