author | blanchet |

Thu Sep 11 21:11:03 2014 +0200 (2014-09-11) | |

changeset 58318 | f95754ca7082 |

parent 58317 | 21fac057681e |

child 58319 | 9228350683d0 |

child 58322 | f13f6e27d68e |

fixed some spelling mistakes

1.1 --- a/src/CTT/Arith.thy Thu Sep 11 20:01:29 2014 +0200 1.2 +++ b/src/CTT/Arith.thy Thu Sep 11 21:11:03 2014 +0200 1.3 @@ -459,7 +459,7 @@ 1.4 apply (erule_tac [3] SumE) 1.5 apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @ 1.6 [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) 1.7 -(*Replace one occurence of b by succ(u mod b). Clumsy!*) 1.8 +(*Replace one occurrence of b by succ(u mod b). Clumsy!*) 1.9 apply (rule add_typingL [THEN trans_elem]) 1.10 apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) 1.11 apply (rule_tac [3] refl_elem)

2.1 --- a/src/Doc/Logics/document/HOL.tex Thu Sep 11 20:01:29 2014 +0200 2.2 +++ b/src/Doc/Logics/document/HOL.tex Thu Sep 11 21:11:03 2014 +0200 2.3 @@ -960,7 +960,7 @@ 2.4 by(simp_tac (simpset() addsplits [split_if]) 1); 2.5 \end{ttbox} 2.6 The effect is that after each round of simplification, one occurrence of 2.7 -\texttt{if} is split acording to \texttt{split_if}, until all occurences of 2.8 +\texttt{if} is split acording to \texttt{split_if}, until all occurrences of 2.9 \texttt{if} have been eliminated. 2.10 2.11 It turns out that using \texttt{split_if} is almost always the right thing to

3.1 --- a/src/HOL/Bali/Eval.thy Thu Sep 11 20:01:29 2014 +0200 3.2 +++ b/src/HOL/Bali/Eval.thy Thu Sep 11 21:11:03 2014 +0200 3.3 @@ -46,7 +46,7 @@ 3.4 statements 3.5 \item the value entry in statement rules is redundant 3.6 \item the value entry in rules is irrelevant in case of exceptions, but its full 3.7 - inclusion helps to make the rule structure independent of exception occurence. 3.8 + inclusion helps to make the rule structure independent of exception occurrence. 3.9 \item as irrelevant value entries are ignored, it does not matter if they are 3.10 unique. 3.11 For simplicity, (fixed) arbitrary values are preferred over "free" values.

4.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Sep 11 20:01:29 2014 +0200 4.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Sep 11 21:11:03 2014 +0200 4.3 @@ -563,7 +563,7 @@ 4.4 apply (frule sym [THEN eq_imp_below, THEN divide_Seq]) 4.5 apply (erule conjE)+ 4.6 4.7 -(* subst divide_Seq in conclusion, but only at the righest occurence *) 4.8 +(* subst divide_Seq in conclusion, but only at the righest occurrence *) 4.9 apply (rule_tac t = "schA" in ssubst) 4.10 back 4.11 back 4.12 @@ -616,7 +616,7 @@ 4.13 apply (frule sym [THEN eq_imp_below, THEN divide_Seq]) 4.14 apply (erule conjE)+ 4.15 4.16 -(* subst divide_Seq in conclusion, but only at the righest occurence *) 4.17 +(* subst divide_Seq in conclusion, but only at the rightmost occurrence *) 4.18 apply (rule_tac t = "schA" in ssubst) 4.19 back 4.20 back 4.21 @@ -782,7 +782,7 @@ 4.22 apply (frule sym [THEN eq_imp_below, THEN divide_Seq]) 4.23 apply (erule conjE)+ 4.24 4.25 -(* subst divide_Seq in conclusion, but only at the righest occurence *) 4.26 +(* subst divide_Seq in conclusion, but only at the rightmost occurrence *) 4.27 apply (rule_tac t = "schB" in ssubst) 4.28 back 4.29 back 4.30 @@ -833,7 +833,7 @@ 4.31 apply (frule sym [THEN eq_imp_below, THEN divide_Seq]) 4.32 apply (erule conjE)+ 4.33 4.34 -(* subst divide_Seq in conclusion, but only at the righest occurence *) 4.35 +(* subst divide_Seq in conclusion, but only at the rightmost occurrence *) 4.36 apply (rule_tac t = "schB" in ssubst) 4.37 back 4.38 back

5.1 --- a/src/HOL/Nominal/Nominal.thy Thu Sep 11 20:01:29 2014 +0200 5.2 +++ b/src/HOL/Nominal/Nominal.thy Thu Sep 11 21:11:03 2014 +0200 5.3 @@ -3650,7 +3650,7 @@ 5.4 method_setup fresh_fun_simp = {* 5.5 Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >> 5.6 (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b)) 5.7 -*} "delete one inner occurence of fresh_fun" 5.8 +*} "delete one inner occurrence of fresh_fun" 5.9 5.10 5.11 (************************************************)

6.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Sep 11 20:01:29 2014 +0200 6.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Sep 11 21:11:03 2014 +0200 6.3 @@ -106,7 +106,7 @@ 6.4 | SOME atom_name => generate_fresh_tac ctxt atom_name 6.5 end) 1; 6.6 6.7 -(* Two substitution tactics which looks for the innermost occurence in 6.8 +(* Two substitution tactics which looks for the innermost occurrence in 6.9 one assumption or in the conclusion *) 6.10 6.11 val search_fun = curry (Seq.flat o uncurry EqSubst.searchf_bt_unify_valid); 6.12 @@ -116,7 +116,7 @@ 6.13 fun subst_inner_asm_tac_aux i ctxt = EqSubst.eqsubst_asm_tac' ctxt search_fun_asm i; 6.14 6.15 (* A tactic to substitute in the first assumption 6.16 - which contains an occurence. *) 6.17 + which contains an occurrence. *) 6.18 6.19 fun subst_inner_asm_tac ctxt th = 6.20 curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux

7.1 --- a/src/Provers/splitter.ML Thu Sep 11 20:01:29 2014 +0200 7.2 +++ b/src/Provers/splitter.ML Thu Sep 11 21:11:03 2014 +0200 7.3 @@ -207,8 +207,8 @@ 7.4 7.5 7.6 (**************************************************************************** 7.7 - Recursively scans term for occurences of Const(key,...) $ ... 7.8 - Returns a list of "split-packs" (one for each occurence of Const(key,...) ) 7.9 + Recursively scans term for occurrences of Const(key,...) $ ... 7.10 + Returns a list of "split-packs" (one for each occurrence of Const(key,...) ) 7.11 7.12 cmap : association list of split-theorems that should be tried. 7.13 The elements have the format (key,(thm,T,n)) , where

8.1 --- a/src/Tools/IsaPlanner/rw_inst.ML Thu Sep 11 20:01:29 2014 +0200 8.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML Thu Sep 11 21:11:03 2014 +0200 8.3 @@ -134,7 +134,7 @@ 8.4 8.5 8.6 (* cross-instantiate the instantiations - ie for each instantiation 8.7 -replace all occurances in other instantiations - no loops are possible 8.8 +replace all occurrences in other instantiations - no loops are possible 8.9 and thus only one-parsing of the instantiations is necessary. *) 8.10 fun cross_inst insts = 8.11 let

9.1 --- a/src/Tools/eqsubst.ML Thu Sep 11 20:01:29 2014 +0200 9.2 +++ b/src/Tools/eqsubst.ML Thu Sep 11 21:11:03 2014 +0200 9.3 @@ -29,7 +29,7 @@ 9.4 val eqsubst_asm_tac': Proof.context -> 9.5 (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic 9.6 val eqsubst_tac: Proof.context -> 9.7 - int list -> (* list of occurences to rewrite, use [0] for any *) 9.8 + int list -> (* list of occurrences to rewrite, use [0] for any *) 9.9 thm list -> int -> tactic 9.10 val eqsubst_tac': Proof.context -> 9.11 (searchinfo -> term -> match Seq.seq) (* search function *) 9.12 @@ -292,7 +292,7 @@ 9.13 in stepthms |> Seq.maps rewrite_with_thm end; 9.14 9.15 9.16 -(* General substitution of multiple occurances using one of 9.17 +(* General substitution of multiple occurrences using one of 9.18 the given theorems *) 9.19 9.20 fun skip_first_occs_search occ srchf sinfo lhs = 9.21 @@ -300,9 +300,9 @@ 9.22 SkipMore _ => Seq.empty 9.23 | SkipSeq ss => Seq.flat ss); 9.24 9.25 -(* The "occs" argument is a list of integers indicating which occurence 9.26 +(* The "occs" argument is a list of integers indicating which occurrence 9.27 w.r.t. the search order, to rewrite. Backtracking will also find later 9.28 -occurences, but all earlier ones are skipped. Thus you can use [0] to 9.29 +occurrences, but all earlier ones are skipped. Thus you can use [0] to 9.30 just find all rewrites. *) 9.31 9.32 fun eqsubst_tac ctxt occs thms i st =

10.1 --- a/src/ZF/Induct/Multiset.thy Thu Sep 11 20:01:29 2014 +0200 10.2 +++ b/src/ZF/Induct/Multiset.thy Thu Sep 11 21:11:03 2014 +0200 10.3 @@ -61,7 +61,7 @@ 10.4 "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})" 10.5 10.6 definition 10.7 - (* Counts the number of occurences of an element in a multiset *) 10.8 + (* Counts the number of occurrences of an element in a multiset *) 10.9 mcount :: "[i, i] => i" where 10.10 "mcount(M, a) == if a \<in> mset_of(M) then M`a else 0" 10.11

11.1 --- a/src/ZF/ex/Limit.thy Thu Sep 11 20:01:29 2014 +0200 11.2 +++ b/src/ZF/ex/Limit.thy Thu Sep 11 21:11:03 2014 +0200 11.3 @@ -1884,7 +1884,7 @@ 11.4 11.5 (* The following theorem is needed/useful due to type check for rel_cfI, 11.6 but also elsewhere. 11.7 - Look for occurences of rel_cfI, rel_DinfI, etc to evaluate the problem. *) 11.8 + Look for occurrences of rel_cfI, rel_DinfI, etc to evaluate the problem. *) 11.9 11.10 lemma lam_Dinf_cont: 11.11 "[| emb_chain(DD,ee); n \<in> nat |]