spelling check
authorpaulson
Sat May 19 12:19:23 2001 +0200 (2001-05-19)
changeset 1131051e70b7bc315
parent 11309 d666f11ca2d4
child 11311 5a659c406465
spelling check
doc-src/TutorialI/Advanced/Partial.thy
doc-src/TutorialI/Advanced/document/Partial.tex
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/Inductive/AB.thy
doc-src/TutorialI/Inductive/document/AB.tex
doc-src/TutorialI/Misc/Option2.thy
doc-src/TutorialI/Misc/Translations.thy
doc-src/TutorialI/Misc/document/Option2.tex
doc-src/TutorialI/Misc/document/Translations.tex
doc-src/TutorialI/Protocol/Event.thy
doc-src/TutorialI/Types/Overloading0.thy
doc-src/TutorialI/Types/Overloading1.thy
doc-src/TutorialI/Types/document/Overloading0.tex
doc-src/TutorialI/Types/document/Overloading1.tex
src/HOL/Auth/Event.thy
     1.1 --- a/doc-src/TutorialI/Advanced/Partial.thy	Fri May 18 17:18:43 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Advanced/Partial.thy	Sat May 19 12:19:23 2001 +0200
     1.3 @@ -2,8 +2,8 @@
     1.4  
     1.5  text{*\noindent Throughout the tutorial we have emphasized the fact
     1.6  that all functions in HOL are total. Hence we cannot hope to define
     1.7 -truly partial functions but must totalize them. A straightforward
     1.8 -totalization is to lift the result type of the function from $\tau$ to
     1.9 +truly partial functions, but must make them total.  A straightforward
    1.10 +method is to lift the result type of the function from $\tau$ to
    1.11  $\tau$~@{text option} (see \ref{sec:option}), where @{term None} is
    1.12  returned if the function is applied to an argument not in its
    1.13  domain. Function @{term assoc} in \S\ref{sec:Trie} is a simple example.
    1.14 @@ -165,7 +165,7 @@
    1.15  text{*\noindent
    1.16  The loop operates on two ``local variables'' @{term x} and @{term x'}
    1.17  containing the ``current'' and the ``next'' value of function @{term f}.
    1.18 -They are initalized with the global @{term x} and @{term"f x"}. At the
    1.19 +They are initialized with the global @{term x} and @{term"f x"}. At the
    1.20  end @{term fst} selects the local @{term x}.
    1.21  
    1.22  Although the definition of tail recursive functions via @{term while} avoids
    1.23 @@ -206,7 +206,7 @@
    1.24  text{* Let us conclude this section on partial functions by a
    1.25  discussion of the merits of the @{term while} combinator. We have
    1.26  already seen that the advantage (if it is one) of not having to
    1.27 -provide a termintion argument when defining a function via @{term
    1.28 +provide a termination argument when defining a function via @{term
    1.29  while} merely puts off the evil hour. On top of that, tail recursive
    1.30  functions tend to be more complicated to reason about. So why use
    1.31  @{term while} at all? The only reason is executability: the recursion
     2.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex	Fri May 18 17:18:43 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Sat May 19 12:19:23 2001 +0200
     2.3 @@ -5,8 +5,8 @@
     2.4  \begin{isamarkuptext}%
     2.5  \noindent Throughout the tutorial we have emphasized the fact
     2.6  that all functions in HOL are total. Hence we cannot hope to define
     2.7 -truly partial functions but must totalize them. A straightforward
     2.8 -totalization is to lift the result type of the function from $\tau$ to
     2.9 +truly partial functions, but must make them total.  A straightforward
    2.10 +method is to lift the result type of the function from $\tau$ to
    2.11  $\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is
    2.12  returned if the function is applied to an argument not in its
    2.13  domain. Function \isa{assoc} in \S\ref{sec:Trie} is a simple example.
    2.14 @@ -172,7 +172,7 @@
    2.15  \noindent
    2.16  The loop operates on two ``local variables'' \isa{x} and \isa{x{\isacharprime}}
    2.17  containing the ``current'' and the ``next'' value of function \isa{f}.
    2.18 -They are initalized with the global \isa{x} and \isa{f\ x}. At the
    2.19 +They are initialized with the global \isa{x} and \isa{f\ x}. At the
    2.20  end \isa{fst} selects the local \isa{x}.
    2.21  
    2.22  Although the definition of tail recursive functions via \isa{while} avoids
    2.23 @@ -215,7 +215,7 @@
    2.24  Let us conclude this section on partial functions by a
    2.25  discussion of the merits of the \isa{while} combinator. We have
    2.26  already seen that the advantage (if it is one) of not having to
    2.27 -provide a termintion argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
    2.28 +provide a termination argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
    2.29  functions tend to be more complicated to reason about. So why use
    2.30  \isa{while} at all? The only reason is executability: the recursion
    2.31  equation for \isa{while} is a directly executable functional
     3.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Fri May 18 17:18:43 2001 +0200
     3.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Sat May 19 12:19:23 2001 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  So far, all datatypes had the property that on the right-hand side of their
     3.5  definition they occurred only at the top-level, i.e.\ directly below a
     3.6  constructor. Now we consider \emph{nested recursion}, where the recursive
     3.7 -datatupe occurs nested in some other datatype (but not inside itself!).
     3.8 +datatype occurs nested in some other datatype (but not inside itself!).
     3.9  Consider the following model of terms
    3.10  where function symbols can be applied to a list of arguments:
    3.11  *}
     4.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Fri May 18 17:18:43 2001 +0200
     4.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Sat May 19 12:19:23 2001 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  So far, all datatypes had the property that on the right-hand side of their
     4.5  definition they occurred only at the top-level, i.e.\ directly below a
     4.6  constructor. Now we consider \emph{nested recursion}, where the recursive
     4.7 -datatupe occurs nested in some other datatype (but not inside itself!).
     4.8 +datatype occurs nested in some other datatype (but not inside itself!).
     4.9  Consider the following model of terms
    4.10  where function symbols can be applied to a list of arguments:%
    4.11  \end{isamarkuptext}%
     5.1 --- a/doc-src/TutorialI/Inductive/AB.thy	Fri May 18 17:18:43 2001 +0200
     5.2 +++ b/doc-src/TutorialI/Inductive/AB.thy	Sat May 19 12:19:23 2001 +0200
     5.3 @@ -285,7 +285,7 @@
     5.4  
     5.5  text{*
     5.6  We conclude this section with a comparison of our proof with 
     5.7 -Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook
     5.8 +Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
     5.9  grammar, for no good reason, excludes the empty word, thus complicating
    5.10  matters just a little bit: they have 8 instead of our 7 productions.
    5.11  
     6.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Fri May 18 17:18:43 2001 +0200
     6.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Sat May 19 12:19:23 2001 +0200
     6.3 @@ -266,7 +266,7 @@
     6.4  \isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
     6.5  \begin{isamarkuptext}%
     6.6  We conclude this section with a comparison of our proof with 
     6.7 -Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook
     6.8 +Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
     6.9  grammar, for no good reason, excludes the empty word, thus complicating
    6.10  matters just a little bit: they have 8 instead of our 7 productions.
    6.11  
     7.1 --- a/doc-src/TutorialI/Misc/Option2.thy	Fri May 18 17:18:43 2001 +0200
     7.2 +++ b/doc-src/TutorialI/Misc/Option2.thy	Sat May 19 12:19:23 2001 +0200
     7.3 @@ -11,7 +11,7 @@
     7.4  datatype 'a option = None | Some 'a;
     7.5  
     7.6  text{*\noindent
     7.7 -Frequently one needs to add a distiguished element to some existing type.
     7.8 +Frequently one needs to add a distinguished element to some existing type.
     7.9  For example, type @{text"t option"} can model the result of a computation that
    7.10  may either terminate with an error (represented by @{term None}) or return
    7.11  some value @{term v} (represented by @{term"Some v"}).
     8.1 --- a/doc-src/TutorialI/Misc/Translations.thy	Fri May 18 17:18:43 2001 +0200
     8.2 +++ b/doc-src/TutorialI/Misc/Translations.thy	Sat May 19 12:19:23 2001 +0200
     8.3 @@ -22,7 +22,7 @@
     8.4  and @{text"\<leftharpoondown>"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
     8.5  for uni-directional translations, which only affect
     8.6  parsing or printing.  We do not want to cover the details of
     8.7 -translations at this point.  We haved mentioned the concept merely because it
     8.8 +translations at this point.  We have mentioned the concept merely because it
     8.9  crops up occasionally: a number of HOL's built-in constructs are defined
    8.10  via translations.  Translations are preferable to definitions when the new 
    8.11  concept is a trivial variation on an existing one.  For example, we
     9.1 --- a/doc-src/TutorialI/Misc/document/Option2.tex	Fri May 18 17:18:43 2001 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/document/Option2.tex	Sat May 19 12:19:23 2001 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4  \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%
     9.5  \begin{isamarkuptext}%
     9.6  \noindent
     9.7 -Frequently one needs to add a distiguished element to some existing type.
     9.8 +Frequently one needs to add a distinguished element to some existing type.
     9.9  For example, type \isa{t\ option} can model the result of a computation that
    9.10  may either terminate with an error (represented by \isa{None}) or return
    9.11  some value \isa{v} (represented by \isa{Some\ v}).
    10.1 --- a/doc-src/TutorialI/Misc/document/Translations.tex	Fri May 18 17:18:43 2001 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/document/Translations.tex	Sat May 19 12:19:23 2001 +0200
    10.3 @@ -24,7 +24,7 @@
    10.4  and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
    10.5  for uni-directional translations, which only affect
    10.6  parsing or printing.  We do not want to cover the details of
    10.7 -translations at this point.  We haved mentioned the concept merely because it
    10.8 +translations at this point.  We have mentioned the concept merely because it
    10.9  crops up occasionally: a number of HOL's built-in constructs are defined
   10.10  via translations.  Translations are preferable to definitions when the new 
   10.11  concept is a trivial variation on an existing one.  For example, we
    11.1 --- a/doc-src/TutorialI/Protocol/Event.thy	Fri May 18 17:18:43 2001 +0200
    11.2 +++ b/doc-src/TutorialI/Protocol/Event.thy	Sat May 19 12:19:23 2001 +0200
    11.3 @@ -27,7 +27,7 @@
    11.4    knows  :: "agent => event list => msg set"
    11.5  
    11.6  
    11.7 -(*"spies" is retained for compability's sake*)
    11.8 +(*"spies" is retained for compatibility's sake*)
    11.9  syntax
   11.10    spies  :: "event list => msg set"
   11.11  
    12.1 --- a/doc-src/TutorialI/Types/Overloading0.thy	Fri May 18 17:18:43 2001 +0200
    12.2 +++ b/doc-src/TutorialI/Types/Overloading0.thy	Sat May 19 12:19:23 2001 +0200
    12.3 @@ -29,7 +29,7 @@
    12.4  left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
    12.5  @{typ"'b \<Rightarrow> 'b"}. The annotation @{text"("}\isacommand{overloaded}@{text")"} tells Isabelle that
    12.6  the definitions do intentionally define @{term[source]inverse} only at
    12.7 -instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely supresses
    12.8 +instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely suppresses
    12.9  warnings to that effect.
   12.10  
   12.11  However, there is nothing to prevent the user from forming terms such as
    13.1 --- a/doc-src/TutorialI/Types/Overloading1.thy	Fri May 18 17:18:43 2001 +0200
    13.2 +++ b/doc-src/TutorialI/Types/Overloading1.thy	Sat May 19 12:19:23 2001 +0200
    13.3 @@ -66,5 +66,5 @@
    13.4  by(simp add: le_bool_def)
    13.5  
    13.6  text{*\noindent
    13.7 -whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped
    13.8 +whereas @{text"[] <<= []"} is not even well-typed. In order to make it well-typed
    13.9  we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
    14.1 --- a/doc-src/TutorialI/Types/document/Overloading0.tex	Fri May 18 17:18:43 2001 +0200
    14.2 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Sat May 19 12:19:23 2001 +0200
    14.3 @@ -33,7 +33,7 @@
    14.4  left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and
    14.5  \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\isacharparenright}} tells Isabelle that
    14.6  the definitions do intentionally define \isa{inverse} only at
    14.7 -instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses
    14.8 +instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses
    14.9  warnings to that effect.
   14.10  
   14.11  However, there is nothing to prevent the user from forming terms such as
    15.1 --- a/doc-src/TutorialI/Types/document/Overloading1.tex	Fri May 18 17:18:43 2001 +0200
    15.2 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Sat May 19 12:19:23 2001 +0200
    15.3 @@ -62,7 +62,7 @@
    15.4  \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
    15.5  \begin{isamarkuptext}%
    15.6  \noindent
    15.7 -whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even welltyped. In order to make it welltyped
    15.8 +whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. In order to make it well-typed
    15.9  we need to make lists a type of class \isa{ordrel}:%
   15.10  \end{isamarkuptext}%
   15.11  \end{isabellebody}%
    16.1 --- a/src/HOL/Auth/Event.thy	Fri May 18 17:18:43 2001 +0200
    16.2 +++ b/src/HOL/Auth/Event.thy	Sat May 19 12:19:23 2001 +0200
    16.3 @@ -27,7 +27,7 @@
    16.4    knows  :: "agent => event list => msg set"
    16.5  
    16.6  
    16.7 -(*"spies" is retained for compability's sake*)
    16.8 +(*"spies" is retained for compatibility's sake*)
    16.9  syntax
   16.10    spies  :: "event list => msg set"
   16.11  
   16.12 @@ -37,8 +37,8 @@
   16.13  
   16.14  axioms
   16.15    (*Spy has access to his own key for spoof messages, but Server is secure*)
   16.16 -  Spy_in_bad     [iff] :    "Spy \<in> bad"
   16.17 -  Server_not_bad [iff] : "Server \<notin> bad"
   16.18 +  Spy_in_bad     [iff] :    "Spy \\<in> bad"
   16.19 +  Server_not_bad [iff] : "Server \\<notin> bad"
   16.20  
   16.21  primrec
   16.22    knows_Nil:   "knows A [] = initState A"
   16.23 @@ -49,7 +49,7 @@
   16.24  	   Says A' B X => insert X (knows Spy evs)
   16.25  	 | Gets A' X => knows Spy evs
   16.26  	 | Notes A' X  => 
   16.27 -	     if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
   16.28 +	     if A' \\<in> bad then insert X (knows Spy evs) else knows Spy evs)
   16.29  	else
   16.30  	(case ev of
   16.31  	   Says A' B X => 
   16.32 @@ -84,6 +84,6 @@
   16.33  method_setup analz_mono_contra = {*
   16.34      Method.no_args
   16.35        (Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
   16.36 -    "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   16.37 +    "for proving theorems of the form X \\<notin> analz (knows Spy evs) --> P"
   16.38  
   16.39  end