--- a/doc-src/TutorialI/Advanced/Partial.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Sat May 19 12:19:23 2001 +0200
@@ -2,8 +2,8 @@
text{*\noindent Throughout the tutorial we have emphasized the fact
that all functions in HOL are total. Hence we cannot hope to define
-truly partial functions but must totalize them. A straightforward
-totalization is to lift the result type of the function from $\tau$ to
+truly partial functions, but must make them total. A straightforward
+method is to lift the result type of the function from $\tau$ to
$\tau$~@{text option} (see \ref{sec:option}), where @{term None} is
returned if the function is applied to an argument not in its
domain. Function @{term assoc} in \S\ref{sec:Trie} is a simple example.
@@ -165,7 +165,7 @@
text{*\noindent
The loop operates on two ``local variables'' @{term x} and @{term x'}
containing the ``current'' and the ``next'' value of function @{term f}.
-They are initalized with the global @{term x} and @{term"f x"}. At the
+They are initialized with the global @{term x} and @{term"f x"}. At the
end @{term fst} selects the local @{term x}.
Although the definition of tail recursive functions via @{term while} avoids
@@ -206,7 +206,7 @@
text{* Let us conclude this section on partial functions by a
discussion of the merits of the @{term while} combinator. We have
already seen that the advantage (if it is one) of not having to
-provide a termintion argument when defining a function via @{term
+provide a termination argument when defining a function via @{term
while} merely puts off the evil hour. On top of that, tail recursive
functions tend to be more complicated to reason about. So why use
@{term while} at all? The only reason is executability: the recursion
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Sat May 19 12:19:23 2001 +0200
@@ -5,8 +5,8 @@
\begin{isamarkuptext}%
\noindent Throughout the tutorial we have emphasized the fact
that all functions in HOL are total. Hence we cannot hope to define
-truly partial functions but must totalize them. A straightforward
-totalization is to lift the result type of the function from $\tau$ to
+truly partial functions, but must make them total. A straightforward
+method is to lift the result type of the function from $\tau$ to
$\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is
returned if the function is applied to an argument not in its
domain. Function \isa{assoc} in \S\ref{sec:Trie} is a simple example.
@@ -172,7 +172,7 @@
\noindent
The loop operates on two ``local variables'' \isa{x} and \isa{x{\isacharprime}}
containing the ``current'' and the ``next'' value of function \isa{f}.
-They are initalized with the global \isa{x} and \isa{f\ x}. At the
+They are initialized with the global \isa{x} and \isa{f\ x}. At the
end \isa{fst} selects the local \isa{x}.
Although the definition of tail recursive functions via \isa{while} avoids
@@ -215,7 +215,7 @@
Let us conclude this section on partial functions by a
discussion of the merits of the \isa{while} combinator. We have
already seen that the advantage (if it is one) of not having to
-provide a termintion argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
+provide a termination argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
functions tend to be more complicated to reason about. So why use
\isa{while} at all? The only reason is executability: the recursion
equation for \isa{while} is a directly executable functional
--- a/doc-src/TutorialI/Datatype/Nested.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Sat May 19 12:19:23 2001 +0200
@@ -6,7 +6,7 @@
So far, all datatypes had the property that on the right-hand side of their
definition they occurred only at the top-level, i.e.\ directly below a
constructor. Now we consider \emph{nested recursion}, where the recursive
-datatupe occurs nested in some other datatype (but not inside itself!).
+datatype occurs nested in some other datatype (but not inside itself!).
Consider the following model of terms
where function symbols can be applied to a list of arguments:
*}
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Sat May 19 12:19:23 2001 +0200
@@ -6,7 +6,7 @@
So far, all datatypes had the property that on the right-hand side of their
definition they occurred only at the top-level, i.e.\ directly below a
constructor. Now we consider \emph{nested recursion}, where the recursive
-datatupe occurs nested in some other datatype (but not inside itself!).
+datatype occurs nested in some other datatype (but not inside itself!).
Consider the following model of terms
where function symbols can be applied to a list of arguments:%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Inductive/AB.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Sat May 19 12:19:23 2001 +0200
@@ -285,7 +285,7 @@
text{*
We conclude this section with a comparison of our proof with
-Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook
+Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
grammar, for no good reason, excludes the empty word, thus complicating
matters just a little bit: they have 8 instead of our 7 productions.
--- a/doc-src/TutorialI/Inductive/document/AB.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Sat May 19 12:19:23 2001 +0200
@@ -266,7 +266,7 @@
\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
\begin{isamarkuptext}%
We conclude this section with a comparison of our proof with
-Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the texbook
+Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
grammar, for no good reason, excludes the empty word, thus complicating
matters just a little bit: they have 8 instead of our 7 productions.
--- a/doc-src/TutorialI/Misc/Option2.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy Sat May 19 12:19:23 2001 +0200
@@ -11,7 +11,7 @@
datatype 'a option = None | Some 'a;
text{*\noindent
-Frequently one needs to add a distiguished element to some existing type.
+Frequently one needs to add a distinguished element to some existing type.
For example, type @{text"t option"} can model the result of a computation that
may either terminate with an error (represented by @{term None}) or return
some value @{term v} (represented by @{term"Some v"}).
--- a/doc-src/TutorialI/Misc/Translations.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Misc/Translations.thy Sat May 19 12:19:23 2001 +0200
@@ -22,7 +22,7 @@
and @{text"\<leftharpoondown>"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
for uni-directional translations, which only affect
parsing or printing. We do not want to cover the details of
-translations at this point. We haved mentioned the concept merely because it
+translations at this point. We have mentioned the concept merely because it
crops up occasionally: a number of HOL's built-in constructs are defined
via translations. Translations are preferable to definitions when the new
concept is a trivial variation on an existing one. For example, we
--- a/doc-src/TutorialI/Misc/document/Option2.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Option2.tex Sat May 19 12:19:23 2001 +0200
@@ -9,7 +9,7 @@
\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%
\begin{isamarkuptext}%
\noindent
-Frequently one needs to add a distiguished element to some existing type.
+Frequently one needs to add a distinguished element to some existing type.
For example, type \isa{t\ option} can model the result of a computation that
may either terminate with an error (represented by \isa{None}) or return
some value \isa{v} (represented by \isa{Some\ v}).
--- a/doc-src/TutorialI/Misc/document/Translations.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Translations.tex Sat May 19 12:19:23 2001 +0200
@@ -24,7 +24,7 @@
and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
for uni-directional translations, which only affect
parsing or printing. We do not want to cover the details of
-translations at this point. We haved mentioned the concept merely because it
+translations at this point. We have mentioned the concept merely because it
crops up occasionally: a number of HOL's built-in constructs are defined
via translations. Translations are preferable to definitions when the new
concept is a trivial variation on an existing one. For example, we
--- a/doc-src/TutorialI/Protocol/Event.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy Sat May 19 12:19:23 2001 +0200
@@ -27,7 +27,7 @@
knows :: "agent => event list => msg set"
-(*"spies" is retained for compability's sake*)
+(*"spies" is retained for compatibility's sake*)
syntax
spies :: "event list => msg set"
--- a/doc-src/TutorialI/Types/Overloading0.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Types/Overloading0.thy Sat May 19 12:19:23 2001 +0200
@@ -29,7 +29,7 @@
left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"("}\isacommand{overloaded}@{text")"} tells Isabelle that
the definitions do intentionally define @{term[source]inverse} only at
-instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely supresses
+instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely suppresses
warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
--- a/doc-src/TutorialI/Types/Overloading1.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Types/Overloading1.thy Sat May 19 12:19:23 2001 +0200
@@ -66,5 +66,5 @@
by(simp add: le_bool_def)
text{*\noindent
-whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped
+whereas @{text"[] <<= []"} is not even well-typed. In order to make it well-typed
we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Sat May 19 12:19:23 2001 +0200
@@ -33,7 +33,7 @@
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
\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\isacharparenright}} tells Isabelle that
the definitions do intentionally define \isa{inverse} only at
-instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses
+instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses
warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Sat May 19 12:19:23 2001 +0200
@@ -62,7 +62,7 @@
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even welltyped. In order to make it welltyped
+whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. In order to make it well-typed
we need to make lists a type of class \isa{ordrel}:%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/src/HOL/Auth/Event.thy Fri May 18 17:18:43 2001 +0200
+++ b/src/HOL/Auth/Event.thy Sat May 19 12:19:23 2001 +0200
@@ -27,7 +27,7 @@
knows :: "agent => event list => msg set"
-(*"spies" is retained for compability's sake*)
+(*"spies" is retained for compatibility's sake*)
syntax
spies :: "event list => msg set"
@@ -37,8 +37,8 @@
axioms
(*Spy has access to his own key for spoof messages, but Server is secure*)
- Spy_in_bad [iff] : "Spy \<in> bad"
- Server_not_bad [iff] : "Server \<notin> bad"
+ Spy_in_bad [iff] : "Spy \\<in> bad"
+ Server_not_bad [iff] : "Server \\<notin> bad"
primrec
knows_Nil: "knows A [] = initState A"
@@ -49,7 +49,7 @@
Says A' B X => insert X (knows Spy evs)
| Gets A' X => knows Spy evs
| Notes A' X =>
- if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs)
+ if A' \\<in> bad then insert X (knows Spy evs) else knows Spy evs)
else
(case ev of
Says A' B X =>
@@ -84,6 +84,6 @@
method_setup analz_mono_contra = {*
Method.no_args
(Method.METHOD (fn facts => REPEAT_FIRST analz_mono_contra_tac)) *}
- "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
+ "for proving theorems of the form X \\<notin> analz (knows Spy evs) --> P"
end