
diff -r c8385f8f7816 -r 3939e7dea202 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 07 23:56:11 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 07 23:56:25 2002 +0100
@@ -90,7 +90,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Mathematical Symbols%
+\isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
 }
 \isamarkuptrue%
 %
@@ -417,7 +417,9 @@
   \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
   accordingly.  \texttt{MySession/document/root.tex} should be also
   adapted at some point; the default version is mostly
-  self-explanatory.
+  self-explanatory.  Note that the \verb,\isabellestyle, enables
+  fine-tuning of the general appearance of characters and mathematical
+  symbols (see also \S\ref{sec:doc-prep-symbols}).
 
   Especially note the standard inclusion of {\LaTeX} packages
   \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
@@ -473,7 +475,7 @@
   \medskip
 
   From the Isabelle perspective, each markup command takes a single
-  text argument (delimited by \verb,",\dots\verb,", or
+  $text$ argument (delimited by \verb,",\dots\verb,", or
   \verb,{,\verb,*,~\dots~\verb,*,\verb,},).  After stripping any
   surrounding white space, the argument is passed to a {\LaTeX} macro
   \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}.  These macros
@@ -543,18 +545,160 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),
+FIXME check
+
+  Source comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),
+  essentially act like white space and do not contribute to the formal
+  text at all.  They mainly serve technical purposes to mark certain
+  oddities or problems with the raw sources.
+
+  In contrast, \bfindex{formal comments} are portions of text that are
+  associated with formal Isabelle/Isar commands (\bfindex{marginal
+  comments}), or even as stanalone paragraphs positioned explicitly
+  within a theory or proof context (\bfindex{text blocks}).
+
+  \medskip Marginal comments are part of each command's concrete
+  syntax \cite{isabelle-ref}; the common form \verb,--,~text, where
+  $text$, delimited by \verb,",\dots\verb,", or
+  \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as usual.  Multiple marginal
+  comments may be given at the same time.  Here is a simple example:
+
+\begin{verbatim}
+  lemma "A --> A"
+    -- "a triviality of propositional logic"
+    -- "(should not really bother)"
+    by (rule impI) -- "implicit assumption step involved here"
+\end{verbatim}
+
+  From the {\LaTeX} view, \verb,--, acts like a markup command, the
+  corresponding macro is \verb,\isamarkupcmt, (of a single argument).
+
+  \medskip The commands \bfindex{text} and \bfindex{txt} both
+  introduce a text block (for theory and proof contexts,
+  respectively), taking a single $text$ argument.  The {\LaTeX} output
+  appears as a free-form text, surrounded with separate paragraphs and
+  additional vertical spacing.  This behavior is determined by the
+  {\LaTeX} environment definitions \verb,isamarkuptext, and
+  \verb,isamarkuptxt,, respectively.  This may be changed via
+  \verb,\renewenvironment,, but it is often sufficient to redefine
+  \verb,\isastyletext, or \verb,\isastyletxt, only, which determine
+  the body text style.
+
+  \medskip The $text$ part of each of the various markup commands
+  considered so far essentially inserts \emph{quoted} material within
+  a formal text, essentially for instruction of the reader only
+  (arbitrary {\LaTeX} macros may be included).
+
+  An \bfindex{antiquotation} is again a formal object that has been
+  embedded into such an informal portion of text.  Typically, the
+  interpretation of an antiquotation is limited to well-formedness
+  checks, with the result being pretty printed into the resulting
+  document output.  So quoted text blocks together with antiquotations
+  provide very handsome means to reference formal entities within
+  informal expositions, with a high level of confidence in the
+  technical details (especially syntax and types).
+
+  The general format of antiquotations is as follows:
+  \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
+  \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
+  for a comma-separated list of $name$ or assignments
+  \texttt{$name$=$value$} of $options$ (see \cite{isabelle-isar-ref}
+  for details).  The syntax of $arguments$ depends on the
+  antiquotation name, it generally follows the same conventions for
+  types, terms, or theorems as in the formal part of a theory.
 
-  FIXME%
+  \medskip Here is an example use of the quotation-antiquotation
+  technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
+
+  \medskip This output has been produced as follows:
+  \begin{ttbox}
+text {\ttlbrace}*
+  Here is an example use of the quotation-antiquotation technique:
+  {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
+*{\ttrbrace}
+  \end{ttbox}
+
+  From the notational change of the ASCII character \verb,%, to the
+  symbol \isa{{\isasymlambda}} we see that the term really got printed by the
+  system --- recall that the document preparation system enables
+  symbolic output by default.
+
+  \medskip In the following example we include an option to enable the
+  \verb,show_types, flag of Isabelle: the antiquotation
+  \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}.  Here type-inference has figured out the
+  most general typings in the present (theory) context.  Within a
+  proof, one may get different results according to typings that have
+  already been figured out in the text so far, say some fixed
+  variables in the main statement given before hand.
+
+  \medskip Several further kinds of antiquotations (and options) are
+  available \cite{isabelle-sys}.  The most commonly used combinations
+  are as follows:
+
+  \medskip
+
+  \begin{tabular}{ll}
+  \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
+  \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
+  \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
+  \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
+  \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
+  \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
+  \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
+  \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
+  \end{tabular}
+
+  \medskip
+
+  Note that \verb,no_vars, given above is \emph{not} an option, but
+  merely an attribute of the theorem argument given here.
+
+  The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
+  particularly interesting.  Embedding uninterpreted text within an
+  informal text body might appear useless at first sight.  Here the
+  key virtue is that the string $s$ is processed as proper Isabelle
+  output, interpreting Isabelle symbols (\S\ref{sec:syntax-symbols})
+  appropriately.
+
+  For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}},
+  according to the standard interpretation of these symbol (cf.\
+  \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
+  mathematical notation in both the formal and informal parts of the
+  document very easily.  Manual {\LaTeX} code leaves more control over
+  the type-setting, but is slightly more tedious.  Also note that
+  Isabelle symbols may be also displayed within the editor buffer of
+  Proof~General.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Symbols and Characters \label{sec:doc-prep-symbols}%
+\isamarkupsubsection{Interpretation of symbols \label{sec:doc-prep-symbols}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME \verb,\isabellestyle,%
+FIXME tune
+
+  According to \S\ref{sec:syntax-symbols}, the smalles syntactic
+  entities of Isabelle text are symbols, a straight-forward
+  generalization of ASCII characters.  Concerning document
+  preperation, symbols are translated uniformly to {\LaTeX} code as
+  follows.
+
+  \begin{enumerate} \item 7-bit ASCII characters: letters
+  \texttt{A\dots Z} and \texttt{a\dots z} are output verbatim, digits
+  are passed as an argument to the \verb,\isadigit, macro, other
+  characters are replaced by specific macros \verb,\isacharXYZ, (see
+  also \texttt{isabelle.sty}).
+
+  \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become
+  \verb,\{\isasym,$XYZ$\verb,}, each (note the additional braces).
+  See \cite[appendix~A]{isabelle-sys} and \texttt{isabellesym.sty} for
+  the collection of predefined standard symbols.
+
+  \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, become
+  \verb,\isactrl,$XYZ$; subsequent symbols may act as arguments, if
+  the corresponding macro is defined accordingly.
+  \end{enumerate}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -626,7 +770,8 @@
 
 \begin{verbatim}
   by (auto(*<*)simp add: int_less_le(*>*))
-\end{verbatim} %(*
+\end{verbatim}
+%(*
 
   \medskip Ignoring portions of printed does demand some care by the
   user.  First of all, the writer is responsible not to obfuscate the




