--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Jul 08 21:55:41 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Jul 08 22:02:15 2008 +0200
@@ -67,7 +67,7 @@
\hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
\hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
- \medskip\noindent Type variables are annotated with (finitly many) classes;
+ \medskip\noindent Type variables are annotated with (finitely many) classes;
these annotations are assertions that a particular polymorphic type
provides definitions for overloaded functions.
--- a/doc-src/Locales/Locales/Examples3.thy Tue Jul 08 21:55:41 2008 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Tue Jul 08 22:02:15 2008 +0200
@@ -356,7 +356,7 @@
that two identical copies of each of the locales @{text
partial_order} and @{text lattice} are imported. This is not the
case! Inheritance paths with identical morphisms are detected and
- the conclusions of the respecitve locales appear only once.
+ the conclusions of the respective locales appear only once.
\begin{figure}
\hrule \vspace{2ex}