--- a/doc-src/TutorialI/Misc/types.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/types.thy Thu Jul 26 16:43:02 2001 +0200
@@ -7,7 +7,7 @@
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theories. Synonyms can be used just like any other
-type:
+type. Here, we declare two constants of type \isa{gate}:
*}
consts nand :: gate
@@ -16,20 +16,21 @@
subsection{*Constant Definitions*}
text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
-The above constants @{term"nand"} and @{term"xor"} are non-recursive and can
-therefore be defined directly by
+The constants @{term"nand"} and @{term"xor"} above are non-recursive and can
+be defined directly:
*}
defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
text{*\noindent%
-where \commdx{defs} is a keyword and
+Here \commdx{defs} is a keyword and
@{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
-Declarations and definitions can also be merged in a \commdx{constdefs}
-command:
+A \commdx{constdefs} command combines the effects of \isacommand{consts} and
+\isacommand{defs}. For instance, we can introduce @{term"nand"} and @{term"xor"} by a
+single command:
*}
constdefs nor :: gate