# HG changeset patch
# User blanchet
# Date 1410462663 -7200
# Node ID f95754ca70825a8f3ce0e6e7f2f8e34aa6596987
# Parent  21fac057681e45ee9defda8adf12a7b5548e7bdb
fixed some spelling mistakes

diff -r 21fac057681e -r f95754ca7082 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/CTT/Arith.thy	Thu Sep 11 21:11:03 2014 +0200
@@ -459,7 +459,7 @@
 apply (erule_tac [3] SumE)
 apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
   [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
-(*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
+(*Replace one occurrence of  b  by succ(u mod b).  Clumsy!*)
 apply (rule add_typingL [THEN trans_elem])
 apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
 apply (rule_tac [3] refl_elem)
diff -r 21fac057681e -r f95754ca7082 src/Doc/Logics/document/HOL.tex
--- a/src/Doc/Logics/document/HOL.tex	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/Doc/Logics/document/HOL.tex	Thu Sep 11 21:11:03 2014 +0200
@@ -960,7 +960,7 @@
 by(simp_tac (simpset() addsplits [split_if]) 1);
 \end{ttbox}
 The effect is that after each round of simplification, one occurrence of
-\texttt{if} is split acording to \texttt{split_if}, until all occurences of
+\texttt{if} is split acording to \texttt{split_if}, until all occurrences of
 \texttt{if} have been eliminated.
 
 It turns out that using \texttt{split_if} is almost always the right thing to
diff -r 21fac057681e -r f95754ca7082 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/HOL/Bali/Eval.thy	Thu Sep 11 21:11:03 2014 +0200
@@ -46,7 +46,7 @@
       statements
 \item the value entry in statement rules is redundant 
 \item the value entry in rules is irrelevant in case of exceptions, but its full
-  inclusion helps to make the rule structure independent of exception occurence.
+  inclusion helps to make the rule structure independent of exception occurrence.
 \item as irrelevant value entries are ignored, it does not matter if they are 
       unique.
   For simplicity, (fixed) arbitrary values are preferred over "free" values.
diff -r 21fac057681e -r f95754ca7082 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Sep 11 21:11:03 2014 +0200
@@ -563,7 +563,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the righest occurrence *)
 apply (rule_tac t = "schA" in ssubst)
 back
 back
@@ -616,7 +616,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
 apply (rule_tac t = "schA" in ssubst)
 back
 back
@@ -782,7 +782,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
 apply (rule_tac t = "schB" in ssubst)
 back
 back
@@ -833,7 +833,7 @@
 apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
-(* subst divide_Seq in conclusion, but only at the righest occurence *)
+(* subst divide_Seq in conclusion, but only at the rightmost occurrence *)
 apply (rule_tac t = "schB" in ssubst)
 back
 back
diff -r 21fac057681e -r f95754ca7082 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 11 21:11:03 2014 +0200
@@ -3650,7 +3650,7 @@
 method_setup fresh_fun_simp = {*
   Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >>
     (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))
-*} "delete one inner occurence of fresh_fun"
+*} "delete one inner occurrence of fresh_fun"
 
 
 (************************************************)
diff -r 21fac057681e -r f95754ca7082 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Sep 11 21:11:03 2014 +0200
@@ -106,7 +106,7 @@
   | SOME atom_name  => generate_fresh_tac ctxt atom_name
   end) 1;
 
-(* Two substitution tactics which looks for the innermost occurence in
+(* Two substitution tactics which looks for the innermost occurrence in
    one assumption or in the conclusion *)
 
 val search_fun = curry (Seq.flat o uncurry EqSubst.searchf_bt_unify_valid);
@@ -116,7 +116,7 @@
 fun subst_inner_asm_tac_aux i ctxt = EqSubst.eqsubst_asm_tac' ctxt search_fun_asm i;
 
 (* A tactic to substitute in the first assumption
-   which contains an occurence. *)
+   which contains an occurrence. *)
 
 fun subst_inner_asm_tac ctxt th =
   curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux
diff -r 21fac057681e -r f95754ca7082 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/Provers/splitter.ML	Thu Sep 11 21:11:03 2014 +0200
@@ -207,8 +207,8 @@
 
 
 (****************************************************************************
-   Recursively scans term for occurences of Const(key,...) $ ...
-   Returns a list of "split-packs" (one for each occurence of Const(key,...) )
+   Recursively scans term for occurrences of Const(key,...) $ ...
+   Returns a list of "split-packs" (one for each occurrence of Const(key,...) )
 
    cmap : association list of split-theorems that should be tried.
           The elements have the format (key,(thm,T,n)) , where
diff -r 21fac057681e -r f95754ca7082 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Sep 11 21:11:03 2014 +0200
@@ -134,7 +134,7 @@
 
 
 (* cross-instantiate the instantiations - ie for each instantiation
-replace all occurances in other instantiations - no loops are possible
+replace all occurrences in other instantiations - no loops are possible
 and thus only one-parsing of the instantiations is necessary. *)
 fun cross_inst insts =
   let
diff -r 21fac057681e -r f95754ca7082 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/Tools/eqsubst.ML	Thu Sep 11 21:11:03 2014 +0200
@@ -29,7 +29,7 @@
   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 *)
@@ -292,7 +292,7 @@
   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 =
@@ -300,9 +300,9 @@
     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 =
diff -r 21fac057681e -r f95754ca7082 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/ZF/Induct/Multiset.thy	Thu Sep 11 21:11:03 2014 +0200
@@ -61,7 +61,7 @@
   "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})"
 
 definition
-  (* Counts the number of occurences of an element in a multiset *)
+  (* Counts the number of occurrences of an element in a multiset *)
   mcount :: "[i, i] => i"  where
   "mcount(M, a) == if a \<in> mset_of(M) then  M`a else 0"
 
diff -r 21fac057681e -r f95754ca7082 src/ZF/ex/Limit.thy
--- a/src/ZF/ex/Limit.thy	Thu Sep 11 20:01:29 2014 +0200
+++ b/src/ZF/ex/Limit.thy	Thu Sep 11 21:11:03 2014 +0200
@@ -1884,7 +1884,7 @@
 
 (* The following theorem is needed/useful due to type check for rel_cfI,
    but also elsewhere.
-   Look for occurences of rel_cfI, rel_DinfI, etc to evaluate the problem. *)
+   Look for occurrences of rel_cfI, rel_DinfI, etc to evaluate the problem. *)
 
 lemma lam_Dinf_cont:
   "[| emb_chain(DD,ee); n \<in> nat |]