doc-src/Exercises/2002/a1/a1.thy
changeset 13844 44f741cdcea3
parent 13739 f5d0a66c8124
     1.1 --- a/doc-src/Exercises/2002/a1/a1.thy	Sat Mar 01 19:19:47 2003 +0100
     1.2 +++ b/doc-src/Exercises/2002/a1/a1.thy	Sat Mar 01 19:34:54 2003 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  
     1.5  text {*
     1.6  Define a function @{term "is_in x xs"} that checks if @{term x} occurs in
     1.7 -@{term xs} vorkommt. Now express @{text is_in} via @{term exs}:
     1.8 +@{term xs}. Now express @{text is_in} via @{term exs}:
     1.9  *}
    1.10  lemma "is_in a xs = Z"
    1.11  (*<*)oops(*>*)
    1.12 @@ -71,4 +71,4 @@
    1.13  
    1.14  (*<*)
    1.15  end
    1.16 -(*>*)
    1.17 \ No newline at end of file
    1.18 +(*>*)