doc-src/TutorialI/Types/Typedef.thy

 @{term three} &::& @{typ"nat set"} \\
 @{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
 @{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
 \end{tabular}
 \end{center}
-Constant @{term three} is just an abbreviation (@{thm[source]three_def}):
-@{thm[display]three_def}
+Constant @{term three} is explicitly defined as the representing set:
+\begin{center}
+@{thm three_def}\hfill(@{thm[source]three_def})
+\end{center}
 The situation is best summarized with the help of the following diagram,
 where squares are types and circles are sets:
 \begin{center}
 \unitlength1mm
 \thicklines

 \end{center}
 Finally, \isacommand{typedef} asserts that @{term Rep_three} is
 surjective on the subset @{term three} and @{term Abs_three} and @{term
 Rep_three} are inverses of each other:
 \begin{center}
-\begin{tabular}{rl}
-@{thm Rep_three[no_vars]} &~~ (@{thm[source]Rep_three}) \\
-@{thm Rep_three_inverse[no_vars]} &~~ (@{thm[source]Rep_three_inverse}) \\
-@{thm Abs_three_inverse[no_vars]} &~~ (@{thm[source]Abs_three_inverse})
+\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
+@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\
+@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\
+@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse})
 \end{tabular}
 \end{center}
 %
 From this example it should be clear what \isacommand{typedef} does
 in general given a name (here @{text three}) and a set