--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 29 13:37:55 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 29 15:47:03 2009 +0100
@@ -132,18 +132,19 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{verbatim}
-reset show_question_marks;
+show_question_marks := false;
\end{verbatim}
at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag reset.
+The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Resetting \verb!show_question_marks! only suppresses question
-marks; variables that end in digits, e.g. @{text"x1"}, are still
-printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
-internal index. This can be avoided by turning the last digit into a
-subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
+suppresses question marks; variables that end in digits,
+e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
+e.g. @{text"x1.0"}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \verb!x\<^isub>1! and
+obtain the much nicer @{text"x\<^isub>1"}. *}
-(*<*)ML"Unsynchronized.reset show_question_marks"(*>*)
+(*<*)ML"show_question_marks := false"(*>*)
subsection {*Qualified names*}
@@ -415,7 +416,7 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
@@ -430,16 +431,16 @@
Likewise, \verb!concl! may be used as a style to show just the
conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
\begin{center}
- @{thm [show_types] hd_Cons_tl}
+ @{thm hd_Cons_tl}
\end{center}
To print just the conclusion,
\begin{center}
- @{thm [show_types] (concl) hd_Cons_tl}
+ @{thm (concl) hd_Cons_tl}
\end{center}
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 29 13:37:55 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 29 15:47:03 2009 +0100
@@ -173,16 +173,17 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{verbatim}
-reset show_question_marks;
+show_question_marks := false;
\end{verbatim}
at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag reset.
+The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Resetting \verb!show_question_marks! only suppresses question
-marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still
-printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their
-internal index. This can be avoided by turning the last digit into a
-subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
+suppresses question marks; variables that end in digits,
+e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isachardot}{\isadigit{0}}},
+e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \verb!x\<^isub>1! and
+obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -537,7 +538,7 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
@@ -552,16 +553,16 @@
Likewise, \verb!concl! may be used as a style to show just the
conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
\begin{center}
- \isa{{\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+ \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
\end{center}
To print just the conclusion,
\begin{center}
- \isa{hd\ {\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+ \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
\end{center}
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex Thu Oct 29 13:37:55 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Thu Oct 29 15:47:03 2009 +0100
@@ -33,7 +33,7 @@
\hyphenation{Isa-belle}
\begin{document}
-\title{\LaTeX\ Sugar for Isabelle documents}
+\title{\LaTeX\ Sugar for Isabelle Documents}
\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
\maketitle