author paulson Sat May 19 12:19:23 2001 +0200 (2001-05-19) changeset 11310 51e70b7bc315 parent 11309 d666f11ca2d4 child 11311 5a659c406465
spelling check
     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.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.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.3 @@ -66,5 +66,5 @@
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.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.3 @@ -62,7 +62,7 @@
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.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