src/Doc/Implementation/Logic.thy

   variables.  Subsequently, we shall use the latter notation instead
   of internal de-Bruijn representation.
 
   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
   \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}
   \qquad