# HG changeset patch
# User wenzelm
# Date 1008082712 -3600
# Node ID 47f79ad602d95def79dfae628967c1cbd2300fdd
# Parent  f9d3c92eae4dd3a86ba940feac3210bf3667e9ac
tuned;

diff -r f9d3c92eae4d -r 47f79ad602d9 doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Tue Dec 11 15:36:28 2001 +0100
+++ b/doc-src/Ref/defining.tex	Tue Dec 11 15:58:32 2001 +0100
@@ -308,34 +308,9 @@
   parse/print translations.
 \end{ttdescription}
 
-Let us demonstrate these functions by inspecting Pure's syntax.  Even that
-is too verbose to display in full.
-\begin{ttbox}\index{*Pure theory}
-Syntax.print_syntax (syn_of Pure.thy);
-{\out lexicon: "!!" "\%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
-{\out logtypes: fun itself}
-{\out prods:}
-{\out   type = tid  (1000)}
-{\out   type = tvar  (1000)}
-{\out   type = id  (1000)}
-{\out   type = tid "::" sort[0]  => "_ofsort" (1000)}
-{\out   type = tvar "::" sort[0]  => "_ofsort" (1000)}
-{\out   \vdots}
-\ttbreak
-{\out print modes: "symbols" "xterm"}
-{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
-{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
-{\out   "_idtyp" "_lambda" "_tapp" "_tappl"}
-{\out parse_rules:}
-{\out parse_translation: "!!" "_K" "_abs" "_aprop"}
-{\out print_translation: "all"}
-{\out print_rules:}
-{\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
-\end{ttbox}
-
-As you can see, the output is divided into labelled sections.  The grammar
-is represented by {\tt lexicon}, {\tt logtypes} and {\tt prods}.  The rest
-refers to syntactic translations and macro expansion.  Here is an
+The output of the above print functions is divided into labelled sections.
+The grammar is represented by {\tt lexicon}, {\tt logtypes} and {\tt prods}.
+The rest refers to syntactic translations and macro expansion.  Here is an
 explanation of the various sections.
 \begin{description}
   \item[{\tt lexicon}] lists the delimiters used for lexical
@@ -684,10 +659,10 @@
 interface).  So changes should be incremental --- adding or deleting
 modes relative to the current value.
 
-Any \ML{} string is a legal print mode identifier, without any
-predeclaration required.  The following names should be considered
-reserved, though: \texttt{""} (yes, the empty string),
-\texttt{symbols}, \texttt{latex}, \texttt{xterm}.
+Any \ML{} string is a legal print mode identifier, without any predeclaration
+required.  The following names should be considered reserved, though:
+\texttt{""} (the empty string), \texttt{symbols}, \texttt{xsymbols}, and
+\texttt{latex}.
 
 There is a separate table of mixfix productions for pretty printing
 associated with each print mode.  The currently active ones are
diff -r f9d3c92eae4d -r 47f79ad602d9 doc-src/System/symbols.tex
--- a/doc-src/System/symbols.tex	Tue Dec 11 15:36:28 2001 +0100
+++ b/doc-src/System/symbols.tex	Tue Dec 11 15:58:32 2001 +0100
@@ -22,7 +22,9 @@
 preparation.
 
 \begin{center}
-  \input{syms}  
+  \begin{isabellebody}
+    \input{syms}  
+  \end{isabellebody}
 \end{center}
 
 %%% Local Variables: 
diff -r f9d3c92eae4d -r 47f79ad602d9 doc-src/System/system.tex
--- a/doc-src/System/system.tex	Tue Dec 11 15:36:28 2001 +0100
+++ b/doc-src/System/system.tex	Tue Dec 11 15:58:32 2001 +0100
@@ -9,7 +9,7 @@
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{wasysym}
 \usepackage{textcomp}
-\usepackage{marvosym}
+\let\RightarrowOrig=\Rightarrow\usepackage{marvosym}\let\Rightarrow=\RightarrowOrig  %bug in marvosym!?
 \usepackage{supertabular}
 \let\intorig=\int  %iman.sty redefines \int
 \usepackage{graphicx,../iman,../extra,../ttbox,../../Distribution/lib/texinputs/isabelle,../../Distribution/lib/texinputs/isabellesym,../pdfsetup}