doc-src/TutorialI/Types/Typedef.thy

 like without \isacommand{datatype}.
 
 Although @{typ three} could be defined in one line, we have chosen this
 example to demonstrate \isacommand{typedef} because its simplicity makes the
 key concepts particularly easy to grasp. If you would like to see a
-nontrivial example that cannot be defined more directly, we recommend the
+non-trivial example that cannot be defined more directly, we recommend the
 definition of \emph{finite multisets} in the HOL Library.
 
 Let us conclude by summarizing the above procedure for defining a new type.
 Given some abstract axiomatic description $P$ of a type $ty$ in terms of a
 set of functions $F$, this involves three steps: