--- a/doc-src/Exercises/2002/a1/a1.thy Sat Mar 01 19:19:47 2003 +0100
+++ b/doc-src/Exercises/2002/a1/a1.thy Sat Mar 01 19:34:54 2003 +0100
@@ -47,7 +47,7 @@
text {*
Define a function @{term "is_in x xs"} that checks if @{term x} occurs in
-@{term xs} vorkommt. Now express @{text is_in} via @{term exs}:
+@{term xs}. Now express @{text is_in} via @{term exs}:
*}
lemma "is_in a xs = Z"
(*<*)oops(*>*)
@@ -71,4 +71,4 @@
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/doc-src/Exercises/2002/a1/generated/a1.tex Sat Mar 01 19:19:47 2003 +0100
+++ b/doc-src/Exercises/2002/a1/generated/a1.tex Sat Mar 01 19:34:54 2003 +0100
@@ -59,7 +59,7 @@
%
\begin{isamarkuptext}%
Define a function \isa{is{\isacharunderscore}in\ x\ xs} that checks if \isa{x} occurs in
-\isa{xs} vorkommt. Now express \isa{is{\isacharunderscore}in} via \isa{exs}:%
+\isa{xs}. Now express \isa{is{\isacharunderscore}in} via \isa{exs}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}is{\isacharunderscore}in\ a\ xs\ {\isacharequal}\ Z{\isachardoublequote}\isamarkupfalse%