diff -r e73723b39c82 -r 4c94f631c595 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Mon Apr 14 23:26:52 2014 +0200
+++ b/src/Doc/Implementation/Logic.thy	Tue Apr 15 00:03:39 2014 +0200
@@ -297,7 +297,7 @@
 
   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
   term according to the structure of atomic terms, abstractions, and
-  applicatins:
+  applications:
   \[
   \infer{@{text "a\<^sub>\<tau> :: \<tau>"}}{}
   \qquad