# HG changeset patch
# User wenzelm
# Date 962474496 -7200
# Node ID 0013b2aa98ddc56af2e0681332622f9bceb7c12b
# Parent  8c8399b9ecaa5912d98fa89d613347a57a3a0277
IGNORE last log message!
added antiquote options "long_names", "eta_contract";

diff -r 8c8399b9ecaa -r 0013b2aa98dd doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sat Jul 01 19:59:24 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sat Jul 01 20:01:36 2000 +0200
@@ -366,7 +366,7 @@
 these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
 \begin{descr}
 \item[$show_types = bool$ and $show_sorts = bool$] control printing of
-  explicit type and sort constraints
+  explicit type and sort constraints.
 \item[$long_names = bool$] forces names of types and constants etc.\ to be
   printed in their fully qualified internal form.
 \item[$eta_contract = bool$] prints terms in $\eta$-contracted form.