# HG changeset patch
# User kleing
# Date 1046543694 -3600
# Node ID 44f741cdcea3e691bf203e7031fb6d40c84ed7da
# Parent  6b5a1dfe8cfc3e5719697a78aac6d0687869c51f
typo

diff -r 6b5a1dfe8cfc -r 44f741cdcea3 doc-src/Exercises/2002/a1/a1.thy
--- 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
+(*>*)
diff -r 6b5a1dfe8cfc -r 44f741cdcea3 doc-src/Exercises/2002/a1/generated/a1.tex
--- 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%