--- a/doc-src/LaTeXsugar/Makefile Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-
-## targets
-
-default: dvi
-
-## paths
-
-SRCPATH = Sugar/document
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = sugar
-
-FILES = Sugar/document/root.tex Sugar/document/root.bib \
- Sugar/document/mathpartir.sty Sugar/document/LaTeXsugar.tex \
- Sugar/document/OptionalSugar.tex Sugar/document/Sugar.tex \
- ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty
-
-GARBAGE = Sugar/document/*.aux Sugar/document/*.log Sugar/document/*.toc \
- Sugar/document/*.idx Sugar/document/*.bbl Sugar/document/*.blg \
- Sugar/document/*.out
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES)
- cd Sugar/document; \
- $(LATEX) root; \
- $(BIBTEX) root; \
- $(LATEX) root; \
- $(LATEX) root
- mv $(SRCPATH)/root.dvi $(NAME).dvi
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES)
- cd Sugar/document; \
- $(PDFLATEX) root; \
- $(BIBTEX) root; \
- $(PDFLATEX) root; \
- $(PDFLATEX) root
- mv $(SRCPATH)/root.pdf $(NAME).pdf
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar.thy Mon Aug 27 22:22:42 2012 +0200
@@ -0,0 +1,461 @@
+(*<*)
+theory Sugar
+imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
+begin
+(*>*)
+
+section "Introduction"
+
+text{* This document is for those Isabelle users who have mastered
+the art of mixing \LaTeX\ text and Isabelle theories and never want to
+typeset a theorem by hand anymore because they have experienced the
+bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
+and seeing Isabelle typeset it for them:
+@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
+No typos, no omissions, no sweat.
+If you have not experienced that joy, read Chapter 4, \emph{Presenting
+Theories}, \cite{LNCS2283} first.
+
+If you have mastered the art of Isabelle's \emph{antiquotations},
+i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
+you may be tempted to think that all readers of the stunning ps or pdf
+documents you can now produce at the drop of a hat will be struck with
+awe at the beauty unfolding in front of their eyes. Until one day you
+come across that very critical of readers known as the ``common referee''.
+He has the nasty habit of refusing to understand unfamiliar notation
+like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
+explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
+\<rbrakk>"} for anything other than denotational semantics is a cardinal sin
+that must be punished by instant rejection.
+
+
+This document shows you how to make Isabelle and \LaTeX\ cooperate to
+produce ordinary looking mathematics that hides the fact that it was
+typeset by a machine. You merely need to load the right files:
+\begin{itemize}
+\item Import theory \texttt{LaTeXsugar} in the header of your own
+theory. You may also want bits of \texttt{OptionalSugar}, which you can
+copy selectively into your own theory or import as a whole. Both
+theories live in \texttt{HOL/Library} and are found automatically.
+
+\item Should you need additional \LaTeX\ packages (the text will tell
+you so), you include them at the beginning of your \LaTeX\ document,
+typically in \texttt{root.tex}. For a start, you should
+\verb!\usepackage{amssymb}! --- otherwise typesetting
+@{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol
+@{text"\<nexists>"} is missing.
+\end{itemize}
+*}
+
+section{* HOL syntax*}
+
+subsection{* Logic *}
+
+text{*
+ The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
+
+The predefined constructs @{text"if"}, @{text"let"} and
+@{text"case"} are set in sans serif font to distinguish them from
+other functions. This improves readability:
+\begin{itemize}
+\item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}.
+\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
+\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
+ @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
+\end{itemize}
+*}
+
+subsection{* Sets *}
+
+text{* Although set syntax in HOL is already close to
+standard, we provide a few further improvements:
+\begin{itemize}
+\item @{term"{x. P}"} instead of @{text"{x. P}"}.
+\item @{term"{}"} instead of @{text"{}"}, where
+ @{term"{}"} is also input syntax.
+\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
+\end{itemize}
+*}
+
+subsection{* Lists *}
+
+text{* If lists are used heavily, the following notations increase readability:
+\begin{itemize}
+\item @{term"x # xs"} instead of @{text"x # xs"},
+ where @{term"x # xs"} is also input syntax.
+If you prefer more space around the $\cdot$ you have to redefine
+\verb!\isasymcdot! in \LaTeX:
+\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
+
+\item @{term"length xs"} instead of @{text"length xs"}.
+\item @{term"nth xs n"} instead of @{text"nth xs n"},
+ the $n$th element of @{text xs}.
+
+\item Human readers are good at converting automatically from lists to
+sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
+conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
+becomes @{prop"x \<in> set xs"}.
+
+\item The @{text"@"} operation associates implicitly to the right,
+which leads to unpleasant line breaks if the term is too long for one
+line. To avoid this, \texttt{OptionalSugar} contains syntax to group
+@{text"@"}-terms to the left before printing, which leads to better
+line breaking behaviour:
+@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
+
+\end{itemize}
+*}
+
+subsection{* Numbers *}
+
+text{* Coercions between numeric types are alien to mathematicians who
+consider, for example, @{typ nat} as a subset of @{typ int}.
+\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
+as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
+@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
+@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
+as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
+hidden. *}
+
+section "Printing theorems"
+
+subsection "Question marks"
+
+text{* If you print anything, especially theorems, containing
+schematic variables they are prefixed with a question mark:
+\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
+you would rather not see the question marks. There is an attribute
+\verb!no_vars! that you can attach to the theorem that turns its
+schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
+results in @{thm conjI[no_vars]}.
+
+This \verb!no_vars! business can become a bit tedious.
+If you would rather never see question marks, simply put
+\begin{quote}
+@{ML "Printer.show_question_marks_default := false"}\verb!;!
+\end{quote}
+at the beginning of your file \texttt{ROOT.ML}.
+The rest of this document is produced with this flag set to \texttt{false}.
+
+Hint: Setting @{ML Printer.show_question_marks_default} 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"}. *}
+
+(*<*)declare [[show_question_marks = false]](*>*)
+
+subsection {*Qualified names*}
+
+text{* If there are multiple declarations of the same name, Isabelle prints
+the qualified name, for example @{text "T.length"}, where @{text T} is the
+theory it is defined in, to distinguish it from the predefined @{const[source]
+"List.length"}. In case there is no danger of confusion, you can insist on
+short names (no qualifiers) by setting the \verb!names_short!
+configuration option in the context.
+*}
+
+subsection {*Variable names\label{sec:varnames}*}
+
+text{* It sometimes happens that you want to change the name of a
+variable in a theorem before printing it. This can easily be achieved
+with the help of Isabelle's instantiation attribute \texttt{where}:
+@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
+\begin{quote}
+\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
+\end{quote}
+To support the ``\_''-notation for irrelevant variables
+the constant \texttt{DUMMY} has been introduced:
+@{thm fst_conv[where b = DUMMY]} is produced by
+\begin{quote}
+\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
+\end{quote}
+Variables that are bound by quantifiers or lambdas cannot be renamed
+like this. Instead, the attribute \texttt{rename\_abs} does the
+job. It expects a list of names or underscores, similar to the
+\texttt{of} attribute:
+\begin{quote}
+\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
+\end{quote}
+produces @{thm split_paired_All[rename_abs _ l r]}.
+*}
+
+subsection "Inference rules"
+
+text{* To print theorems as inference rules you need to include Didier
+R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
+for typesetting inference rules in your \LaTeX\ file.
+
+Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
+@{thm[mode=Rule] conjI}, even in the middle of a sentence.
+If you prefer your inference rule on a separate line, maybe with a name,
+\begin{center}
+@{thm[mode=Rule] conjI} {\sc conjI}
+\end{center}
+is produced by
+\begin{quote}
+\verb!\begin{center}!\\
+\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
+\verb!\end{center}!
+\end{quote}
+It is not recommended to use the standard \texttt{display} option
+together with \texttt{Rule} because centering does not work and because
+the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
+clash.
+
+Of course you can display multiple rules in this fashion:
+\begin{quote}
+\verb!\begin{center}!\\
+\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
+\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
+\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
+\verb!\end{center}!
+\end{quote}
+yields
+\begin{center}\small
+@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
+@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
+@{thm[mode=Rule] disjI2} {\sc disjI$_2$}
+\end{center}
+
+The \texttt{mathpartir} package copes well if there are too many
+premises for one line:
+\begin{center}
+@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
+ G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
+\end{center}
+
+Limitations: 1. Premises and conclusion must each not be longer than
+the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again
+displayed with a horizontal line, which looks at least unusual.
+
+
+In case you print theorems without premises no rule will be printed by the
+\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
+\begin{quote}
+\verb!\begin{center}!\\
+\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
+\verb!\end{center}!
+\end{quote}
+yields
+\begin{center}
+@{thm[mode=Axiom] refl} {\sc refl}
+\end{center}
+*}
+
+subsection "Displays and font sizes"
+
+text{* When displaying theorems with the \texttt{display} option, e.g.
+\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
+set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
+which is also the style that regular theory text is set in, e.g. *}
+
+lemma "t = t"
+(*<*)oops(*>*)
+
+text{* \noindent Otherwise \verb!\isastyleminor! is used,
+which does not modify the font size (assuming you stick to the default
+\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
+normal font size throughout your text, include
+\begin{quote}
+\verb!\renewcommand{\isastyle}{\isastyleminor}!
+\end{quote}
+in \texttt{root.tex}. On the other hand, if you like the small font,
+just put \verb!\isastyle! in front of the text in question,
+e.g.\ at the start of one of the center-environments above.
+
+The advantage of the display option is that you can display a whole
+list of theorems in one go. For example,
+\verb!@!\verb!{thm[display] append.simps}!
+generates @{thm[display] append.simps}
+*}
+
+subsection "If-then"
+
+text{* If you prefer a fake ``natural language'' style you can produce
+the body of
+\newtheorem{theorem}{Theorem}
+\begin{theorem}
+@{thm[mode=IfThen] le_trans}
+\end{theorem}
+by typing
+\begin{quote}
+\verb!@!\verb!{thm[mode=IfThen] le_trans}!
+\end{quote}
+
+In order to prevent odd line breaks, the premises are put into boxes.
+At times this is too drastic:
+\begin{theorem}
+@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
+\end{theorem}
+In which case you should use \texttt{IfThenNoBox} instead of
+\texttt{IfThen}:
+\begin{theorem}
+@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
+\end{theorem}
+*}
+
+subsection{* Doing it yourself\label{sec:yourself}*}
+
+text{* If for some reason you want or need to present theorems your
+own way, you can extract the premises and the conclusion explicitly
+and combine them as you like:
+\begin{itemize}
+\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
+prints premise 1 of $thm$.
+\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
+prints the conclusion of $thm$.
+\end{itemize}
+For example, ``from @{thm (prem 2) conjI} and
+@{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
+is produced by
+\begin{quote}
+\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
+\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
+\end{quote}
+Thus you can rearrange or hide premises and typeset the theorem as you like.
+Styles like \verb!(prem 1)! are a general mechanism explained
+in \S\ref{sec:styles}.
+*}
+
+subsection "Patterns"
+
+text {*
+
+ In \S\ref{sec:varnames} we shows how to create patterns containing
+ ``@{term DUMMY}''.
+ You can drive this game even further and extend the syntax of let
+ bindings such that certain functions like @{term fst}, @{term hd},
+ etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
+ following:
+
+ \begin{center}
+ \begin{tabular}{l@ {~~produced by~~}l}
+ @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
+ @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
+ @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
+ @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
+ @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
+ \end{tabular}
+ \end{center}
+*}
+
+section "Proofs"
+
+text {* Full proofs, even if written in beautiful Isar style, are
+likely to be too long and detailed to be included in conference
+papers, but some key lemmas might be of interest.
+It is usually easiest to put them in figures like the one in Fig.\
+\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
+*}
+text_raw {*
+ \begin{figure}
+ \begin{center}\begin{minipage}{0.6\textwidth}
+ \isastyleminor\isamarkuptrue
+*}
+lemma True
+proof -
+ -- "pretty trivial"
+ show True by force
+qed
+text_raw {*
+ \end{minipage}\end{center}
+ \caption{Example proof in a figure.}\label{fig:proof}
+ \end{figure}
+*}
+text {*
+
+\begin{quote}
+\small
+\verb!text_raw {!\verb!*!\\
+\verb! \begin{figure}!\\
+\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
+\verb! \isastyleminor\isamarkuptrue!\\
+\verb!*!\verb!}!\\
+\verb!lemma True!\\
+\verb!proof -!\\
+\verb! -- "pretty trivial"!\\
+\verb! show True by force!\\
+\verb!qed!\\
+\verb!text_raw {!\verb!*!\\
+\verb! \end{minipage}\end{center}!\\
+\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
+\verb! \end{figure}!\\
+\verb!*!\verb!}!
+\end{quote}
+
+Other theory text, e.g.\ definitions, can be put in figures, too.
+*}
+
+section {*Styles\label{sec:styles}*}
+
+text {*
+ The \verb!thm! antiquotation works nicely for single theorems, but
+ sets of equations as used in definitions are more difficult to
+ typeset nicely: people tend to prefer aligned @{text "="} signs.
+
+ To deal with such cases where it is desirable to dive into the structure
+ of terms and theorems, Isabelle offers antiquotations featuring
+ ``styles'':
+
+ \begin{quote}
+ \verb!@!\verb!{thm (style) thm}!\\
+ \verb!@!\verb!{prop (style) thm}!\\
+ \verb!@!\verb!{term (style) term}!\\
+ \verb!@!\verb!{term_type (style) term}!\\
+ \verb!@!\verb!{typeof (style) term}!\\
+ \end{quote}
+
+ A ``style'' is a transformation of a term. There are predefined
+ styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
+ For example,
+ the output
+ \begin{center}
+ \begin{tabular}{l@ {~~@{text "="}~~}l}
+ @{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
+ @{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
+ \end{tabular}
+ \end{center}
+ is produced by the following code:
+ \begin{quote}
+ \verb!\begin{center}!\\
+ \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
+ \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
+ \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
+ \verb!\end{tabular}!\\
+ \verb!\end{center}!
+ \end{quote}
+ Note the space between \verb!@! and \verb!{! in the tabular argument.
+ It prevents Isabelle from interpreting \verb!@ {~~...~~}!
+ as an antiquotation. The styles \verb!lhs! and \verb!rhs!
+ extract the left hand side (or right hand side respectively) from the
+ conclusion of propositions consisting of a binary operator
+ (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
+
+ 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 hd_Cons_tl}
+ \end{center}
+ To print just the conclusion,
+ \begin{center}
+ @{thm (concl) hd_Cons_tl}
+ \end{center}
+ type
+ \begin{quote}
+ \verb!\begin{center}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
+ \verb!\end{center}!
+ \end{quote}
+ Beware that any options must be placed \emph{before}
+ the style, as in this example.
+
+ Further use cases can be found in \S\ref{sec:yourself}.
+ If you are not afraid of ML, you may also define your own styles.
+ Have a look at module @{ML_struct Term_Style}.
+*}
+
+(*<*)
+end
+(*>*)
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,461 +0,0 @@
-(*<*)
-theory Sugar
-imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
-begin
-(*>*)
-
-section "Introduction"
-
-text{* This document is for those Isabelle users who have mastered
-the art of mixing \LaTeX\ text and Isabelle theories and never want to
-typeset a theorem by hand anymore because they have experienced the
-bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
-and seeing Isabelle typeset it for them:
-@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
-No typos, no omissions, no sweat.
-If you have not experienced that joy, read Chapter 4, \emph{Presenting
-Theories}, \cite{LNCS2283} first.
-
-If you have mastered the art of Isabelle's \emph{antiquotations},
-i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
-you may be tempted to think that all readers of the stunning ps or pdf
-documents you can now produce at the drop of a hat will be struck with
-awe at the beauty unfolding in front of their eyes. Until one day you
-come across that very critical of readers known as the ``common referee''.
-He has the nasty habit of refusing to understand unfamiliar notation
-like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
-explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
-\<rbrakk>"} for anything other than denotational semantics is a cardinal sin
-that must be punished by instant rejection.
-
-
-This document shows you how to make Isabelle and \LaTeX\ cooperate to
-produce ordinary looking mathematics that hides the fact that it was
-typeset by a machine. You merely need to load the right files:
-\begin{itemize}
-\item Import theory \texttt{LaTeXsugar} in the header of your own
-theory. You may also want bits of \texttt{OptionalSugar}, which you can
-copy selectively into your own theory or import as a whole. Both
-theories live in \texttt{HOL/Library} and are found automatically.
-
-\item Should you need additional \LaTeX\ packages (the text will tell
-you so), you include them at the beginning of your \LaTeX\ document,
-typically in \texttt{root.tex}. For a start, you should
-\verb!\usepackage{amssymb}! --- otherwise typesetting
-@{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol
-@{text"\<nexists>"} is missing.
-\end{itemize}
-*}
-
-section{* HOL syntax*}
-
-subsection{* Logic *}
-
-text{*
- The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
-
-The predefined constructs @{text"if"}, @{text"let"} and
-@{text"case"} are set in sans serif font to distinguish them from
-other functions. This improves readability:
-\begin{itemize}
-\item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}.
-\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
-\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
- @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
-\end{itemize}
-*}
-
-subsection{* Sets *}
-
-text{* Although set syntax in HOL is already close to
-standard, we provide a few further improvements:
-\begin{itemize}
-\item @{term"{x. P}"} instead of @{text"{x. P}"}.
-\item @{term"{}"} instead of @{text"{}"}, where
- @{term"{}"} is also input syntax.
-\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
-\end{itemize}
-*}
-
-subsection{* Lists *}
-
-text{* If lists are used heavily, the following notations increase readability:
-\begin{itemize}
-\item @{term"x # xs"} instead of @{text"x # xs"},
- where @{term"x # xs"} is also input syntax.
-If you prefer more space around the $\cdot$ you have to redefine
-\verb!\isasymcdot! in \LaTeX:
-\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
-
-\item @{term"length xs"} instead of @{text"length xs"}.
-\item @{term"nth xs n"} instead of @{text"nth xs n"},
- the $n$th element of @{text xs}.
-
-\item Human readers are good at converting automatically from lists to
-sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
-conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
-becomes @{prop"x \<in> set xs"}.
-
-\item The @{text"@"} operation associates implicitly to the right,
-which leads to unpleasant line breaks if the term is too long for one
-line. To avoid this, \texttt{OptionalSugar} contains syntax to group
-@{text"@"}-terms to the left before printing, which leads to better
-line breaking behaviour:
-@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
-
-\end{itemize}
-*}
-
-subsection{* Numbers *}
-
-text{* Coercions between numeric types are alien to mathematicians who
-consider, for example, @{typ nat} as a subset of @{typ int}.
-\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
-as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
-@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
-@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
-as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
-hidden. *}
-
-section "Printing theorems"
-
-subsection "Question marks"
-
-text{* If you print anything, especially theorems, containing
-schematic variables they are prefixed with a question mark:
-\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
-you would rather not see the question marks. There is an attribute
-\verb!no_vars! that you can attach to the theorem that turns its
-schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
-results in @{thm conjI[no_vars]}.
-
-This \verb!no_vars! business can become a bit tedious.
-If you would rather never see question marks, simply put
-\begin{quote}
-@{ML "Printer.show_question_marks_default := false"}\verb!;!
-\end{quote}
-at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag set to \texttt{false}.
-
-Hint: Setting @{ML Printer.show_question_marks_default} 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"}. *}
-
-(*<*)declare [[show_question_marks = false]](*>*)
-
-subsection {*Qualified names*}
-
-text{* If there are multiple declarations of the same name, Isabelle prints
-the qualified name, for example @{text "T.length"}, where @{text T} is the
-theory it is defined in, to distinguish it from the predefined @{const[source]
-"List.length"}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting the \verb!names_short!
-configuration option in the context.
-*}
-
-subsection {*Variable names\label{sec:varnames}*}
-
-text{* It sometimes happens that you want to change the name of a
-variable in a theorem before printing it. This can easily be achieved
-with the help of Isabelle's instantiation attribute \texttt{where}:
-@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
-\begin{quote}
-\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
-\end{quote}
-To support the ``\_''-notation for irrelevant variables
-the constant \texttt{DUMMY} has been introduced:
-@{thm fst_conv[where b = DUMMY]} is produced by
-\begin{quote}
-\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
-\end{quote}
-Variables that are bound by quantifiers or lambdas cannot be renamed
-like this. Instead, the attribute \texttt{rename\_abs} does the
-job. It expects a list of names or underscores, similar to the
-\texttt{of} attribute:
-\begin{quote}
-\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
-\end{quote}
-produces @{thm split_paired_All[rename_abs _ l r]}.
-*}
-
-subsection "Inference rules"
-
-text{* To print theorems as inference rules you need to include Didier
-R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
-for typesetting inference rules in your \LaTeX\ file.
-
-Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
-@{thm[mode=Rule] conjI}, even in the middle of a sentence.
-If you prefer your inference rule on a separate line, maybe with a name,
-\begin{center}
-@{thm[mode=Rule] conjI} {\sc conjI}
-\end{center}
-is produced by
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
-\verb!\end{center}!
-\end{quote}
-It is not recommended to use the standard \texttt{display} option
-together with \texttt{Rule} because centering does not work and because
-the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
-clash.
-
-Of course you can display multiple rules in this fashion:
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
-\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
-\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
-\verb!\end{center}!
-\end{quote}
-yields
-\begin{center}\small
-@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
-@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
-@{thm[mode=Rule] disjI2} {\sc disjI$_2$}
-\end{center}
-
-The \texttt{mathpartir} package copes well if there are too many
-premises for one line:
-\begin{center}
-@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
- G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
-\end{center}
-
-Limitations: 1. Premises and conclusion must each not be longer than
-the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again
-displayed with a horizontal line, which looks at least unusual.
-
-
-In case you print theorems without premises no rule will be printed by the
-\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
-\verb!\end{center}!
-\end{quote}
-yields
-\begin{center}
-@{thm[mode=Axiom] refl} {\sc refl}
-\end{center}
-*}
-
-subsection "Displays and font sizes"
-
-text{* When displaying theorems with the \texttt{display} option, e.g.
-\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
-set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
-which is also the style that regular theory text is set in, e.g. *}
-
-lemma "t = t"
-(*<*)oops(*>*)
-
-text{* \noindent Otherwise \verb!\isastyleminor! is used,
-which does not modify the font size (assuming you stick to the default
-\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
-normal font size throughout your text, include
-\begin{quote}
-\verb!\renewcommand{\isastyle}{\isastyleminor}!
-\end{quote}
-in \texttt{root.tex}. On the other hand, if you like the small font,
-just put \verb!\isastyle! in front of the text in question,
-e.g.\ at the start of one of the center-environments above.
-
-The advantage of the display option is that you can display a whole
-list of theorems in one go. For example,
-\verb!@!\verb!{thm[display] append.simps}!
-generates @{thm[display] append.simps}
-*}
-
-subsection "If-then"
-
-text{* If you prefer a fake ``natural language'' style you can produce
-the body of
-\newtheorem{theorem}{Theorem}
-\begin{theorem}
-@{thm[mode=IfThen] le_trans}
-\end{theorem}
-by typing
-\begin{quote}
-\verb!@!\verb!{thm[mode=IfThen] le_trans}!
-\end{quote}
-
-In order to prevent odd line breaks, the premises are put into boxes.
-At times this is too drastic:
-\begin{theorem}
-@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
-\end{theorem}
-In which case you should use \texttt{IfThenNoBox} instead of
-\texttt{IfThen}:
-\begin{theorem}
-@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
-\end{theorem}
-*}
-
-subsection{* Doing it yourself\label{sec:yourself}*}
-
-text{* If for some reason you want or need to present theorems your
-own way, you can extract the premises and the conclusion explicitly
-and combine them as you like:
-\begin{itemize}
-\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
-prints premise 1 of $thm$.
-\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
-prints the conclusion of $thm$.
-\end{itemize}
-For example, ``from @{thm (prem 2) conjI} and
-@{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
-is produced by
-\begin{quote}
-\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
-\end{quote}
-Thus you can rearrange or hide premises and typeset the theorem as you like.
-Styles like \verb!(prem 1)! are a general mechanism explained
-in \S\ref{sec:styles}.
-*}
-
-subsection "Patterns"
-
-text {*
-
- In \S\ref{sec:varnames} we shows how to create patterns containing
- ``@{term DUMMY}''.
- You can drive this game even further and extend the syntax of let
- bindings such that certain functions like @{term fst}, @{term hd},
- etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
- following:
-
- \begin{center}
- \begin{tabular}{l@ {~~produced by~~}l}
- @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
- @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
- @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
- @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
- @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
- \end{tabular}
- \end{center}
-*}
-
-section "Proofs"
-
-text {* Full proofs, even if written in beautiful Isar style, are
-likely to be too long and detailed to be included in conference
-papers, but some key lemmas might be of interest.
-It is usually easiest to put them in figures like the one in Fig.\
-\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
-*}
-text_raw {*
- \begin{figure}
- \begin{center}\begin{minipage}{0.6\textwidth}
- \isastyleminor\isamarkuptrue
-*}
-lemma True
-proof -
- -- "pretty trivial"
- show True by force
-qed
-text_raw {*
- \end{minipage}\end{center}
- \caption{Example proof in a figure.}\label{fig:proof}
- \end{figure}
-*}
-text {*
-
-\begin{quote}
-\small
-\verb!text_raw {!\verb!*!\\
-\verb! \begin{figure}!\\
-\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
-\verb! \isastyleminor\isamarkuptrue!\\
-\verb!*!\verb!}!\\
-\verb!lemma True!\\
-\verb!proof -!\\
-\verb! -- "pretty trivial"!\\
-\verb! show True by force!\\
-\verb!qed!\\
-\verb!text_raw {!\verb!*!\\
-\verb! \end{minipage}\end{center}!\\
-\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
-\verb! \end{figure}!\\
-\verb!*!\verb!}!
-\end{quote}
-
-Other theory text, e.g.\ definitions, can be put in figures, too.
-*}
-
-section {*Styles\label{sec:styles}*}
-
-text {*
- The \verb!thm! antiquotation works nicely for single theorems, but
- sets of equations as used in definitions are more difficult to
- typeset nicely: people tend to prefer aligned @{text "="} signs.
-
- To deal with such cases where it is desirable to dive into the structure
- of terms and theorems, Isabelle offers antiquotations featuring
- ``styles'':
-
- \begin{quote}
- \verb!@!\verb!{thm (style) thm}!\\
- \verb!@!\verb!{prop (style) thm}!\\
- \verb!@!\verb!{term (style) term}!\\
- \verb!@!\verb!{term_type (style) term}!\\
- \verb!@!\verb!{typeof (style) term}!\\
- \end{quote}
-
- A ``style'' is a transformation of a term. There are predefined
- styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
- For example,
- the output
- \begin{center}
- \begin{tabular}{l@ {~~@{text "="}~~}l}
- @{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
- @{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
- \end{tabular}
- \end{center}
- is produced by the following code:
- \begin{quote}
- \verb!\begin{center}!\\
- \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
- \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
- \verb!\end{tabular}!\\
- \verb!\end{center}!
- \end{quote}
- Note the space between \verb!@! and \verb!{! in the tabular argument.
- It prevents Isabelle from interpreting \verb!@ {~~...~~}!
- as an antiquotation. The styles \verb!lhs! and \verb!rhs!
- extract the left hand side (or right hand side respectively) from the
- conclusion of propositions consisting of a binary operator
- (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
-
- 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 hd_Cons_tl}
- \end{center}
- To print just the conclusion,
- \begin{center}
- @{thm (concl) hd_Cons_tl}
- \end{center}
- type
- \begin{quote}
- \verb!\begin{center}!\\
- \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
- \verb!\end{center}!
- \end{quote}
- Beware that any options must be placed \emph{before}
- the style, as in this example.
-
- Further use cases can be found in \S\ref{sec:yourself}.
- If you are not afraid of ML, you may also define your own styles.
- Have a look at module @{ML_struct Term_Style}.
-*}
-
-(*<*)
-end
-(*>*)
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,585 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Sugar}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Introduction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-This document is for those Isabelle users who have mastered
-the art of mixing \LaTeX\ text and Isabelle theories and never want to
-typeset a theorem by hand anymore because they have experienced the
-bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
-and seeing Isabelle typeset it for them:
-\begin{isabelle}%
-{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C53756D3E}{\isasymSum}}y{\isaliteral{5C3C696E3E}{\isasymin}}B{\isaliteral{2E}{\isachardot}}\ f\ x\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E3E}{\isasymin}}A\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ B{\isaliteral{2E}{\isachardot}}\ f\ x\ y{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-No typos, no omissions, no sweat.
-If you have not experienced that joy, read Chapter 4, \emph{Presenting
-Theories}, \cite{LNCS2283} first.
-
-If you have mastered the art of Isabelle's \emph{antiquotations},
-i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
-you may be tempted to think that all readers of the stunning ps or pdf
-documents you can now produce at the drop of a hat will be struck with
-awe at the beauty unfolding in front of their eyes. Until one day you
-come across that very critical of readers known as the ``common referee''.
-He has the nasty habit of refusing to understand unfamiliar notation
-like Isabelle's infamous \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} no matter how many times you
-explain it in your paper. Even worse, he thinks that using \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}} for anything other than denotational semantics is a cardinal sin
-that must be punished by instant rejection.
-
-
-This document shows you how to make Isabelle and \LaTeX\ cooperate to
-produce ordinary looking mathematics that hides the fact that it was
-typeset by a machine. You merely need to load the right files:
-\begin{itemize}
-\item Import theory \texttt{LaTeXsugar} in the header of your own
-theory. You may also want bits of \texttt{OptionalSugar}, which you can
-copy selectively into your own theory or import as a whole. Both
-theories live in \texttt{HOL/Library} and are found automatically.
-
-\item Should you need additional \LaTeX\ packages (the text will tell
-you so), you include them at the beginning of your \LaTeX\ document,
-typically in \texttt{root.tex}. For a start, you should
-\verb!\usepackage{amssymb}! --- otherwise typesetting
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} will fail because the AMS symbol
-\isa{{\isaliteral{5C3C6E6578697374733E}{\isasymnexists}}} is missing.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{HOL syntax%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Logic%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The formula \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is typeset as \isa{{\isaliteral{5C3C6E6578697374733E}{\isasymnexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x}.
-
-The predefined constructs \isa{if}, \isa{let} and
-\isa{case} are set in sans serif font to distinguish them from
-other functions. This improves readability:
-\begin{itemize}
-\item \isa{\textsf{if}\ b\ \textsf{then}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \textsf{else}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of \isa{if\ b\ then\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ else\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.
-\item \isa{\textsf{let}\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \textsf{in}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of \isa{let\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ in\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.
-\item \isa{\textsf{case}\ x\ \textsf{of}\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of\\
- \isa{case\ x\ of\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Sets%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Although set syntax in HOL is already close to
-standard, we provide a few further improvements:
-\begin{itemize}
-\item \isa{{\isaliteral{7B}{\isacharbraceleft}}x\ {\isaliteral{7C}{\isacharbar}}\ P{\isaliteral{7D}{\isacharbraceright}}} instead of \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}}.
-\item \isa{{\isaliteral{5C3C656D7074797365743E}{\isasymemptyset}}} instead of \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}}, where
- \isa{{\isaliteral{5C3C656D7074797365743E}{\isasymemptyset}}} is also input syntax.
-\item \isa{{\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M} instead of \isa{insert\ a\ {\isaliteral{28}{\isacharparenleft}}insert\ b\ {\isaliteral{28}{\isacharparenleft}}insert\ c\ M{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lists%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If lists are used heavily, the following notations increase readability:
-\begin{itemize}
-\item \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs} instead of \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs},
- where \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs} is also input syntax.
-If you prefer more space around the $\cdot$ you have to redefine
-\verb!\isasymcdot! in \LaTeX:
-\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
-
-\item \isa{{\isaliteral{7C}{\isacharbar}}xs{\isaliteral{7C}{\isacharbar}}} instead of \isa{length\ xs}.
-\item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n},
- the $n$th element of \isa{xs}.
-
-\item Human readers are good at converting automatically from lists to
-sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
-conversion function \isa{set}: for example, \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ xs{\isaliteral{22}{\isachardoublequote}}}
-becomes \isa{x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ xs}.
-
-\item The \isa{{\isaliteral{40}{\isacharat}}} operation associates implicitly to the right,
-which leads to unpleasant line breaks if the term is too long for one
-line. To avoid this, \texttt{OptionalSugar} contains syntax to group
-\isa{{\isaliteral{40}{\isacharat}}}-terms to the left before printing, which leads to better
-line breaking behaviour:
-\begin{isabelle}%
-term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{0}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{4}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{5}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{6}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{7}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{8}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{9}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{0}}%
-\end{isabelle}
-
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Numbers%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Coercions between numeric types are alien to mathematicians who
-consider, for example, \isa{nat} as a subset of \isa{int}.
-\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
-as \isa{int} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}. For example,
-\isa{{\isaliteral{22}{\isachardoublequote}}int\ {\isadigit{5}}{\isaliteral{22}{\isachardoublequote}}} is printed as \isa{{\isadigit{5}}}. Embeddings of types
-\isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such
-as \isa{nat} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} are not and should not be
-hidden.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Printing theorems%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Question marks%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you print anything, especially theorems, containing
-schematic variables they are prefixed with a question mark:
-\verb!@!\verb!{thm conjI}! results in \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q}. Most of the time
-you would rather not see the question marks. There is an attribute
-\verb!no_vars! that you can attach to the theorem that turns its
-schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
-results in \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P{\isaliteral{3B}{\isacharsemicolon}}\ Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}.
-
-This \verb!no_vars! business can become a bit tedious.
-If you would rather never see question marks, simply put
-\begin{quote}
-\verb|Printer.show_question_marks_default := false|\verb!;!
-\end{quote}
-at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag set to \texttt{false}.
-
-Hint: Setting \verb|Printer.show_question_marks_default| 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{{\isaliteral{2E}{\isachardot}}{\isadigit{0}}},
-e.g. \isa{x{\isadigit{1}}{\isaliteral{2E}{\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\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Qualified names%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If there are multiple declarations of the same name, Isabelle prints
-the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
-theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting the \verb!names_short!
-configuration option in the context.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Variable names\label{sec:varnames}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-It sometimes happens that you want to change the name of a
-variable in a theorem before printing it. This can easily be achieved
-with the help of Isabelle's instantiation attribute \texttt{where}:
-\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C7073693E}{\isasympsi}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C7073693E}{\isasympsi}}} is the result of
-\begin{quote}
-\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
-\end{quote}
-To support the ``\_''-notation for irrelevant variables
-the constant \texttt{DUMMY} has been introduced:
-\isa{fst\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ \_{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a} is produced by
-\begin{quote}
-\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
-\end{quote}
-Variables that are bound by quantifiers or lambdas cannot be renamed
-like this. Instead, the attribute \texttt{rename\_abs} does the
-job. It expects a list of names or underscores, similar to the
-\texttt{of} attribute:
-\begin{quote}
-\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
-\end{quote}
-produces \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}l\ r{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Inference rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-To print theorems as inference rules you need to include Didier
-R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
-for typesetting inference rules in your \LaTeX\ file.
-
-Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}}, even in the middle of a sentence.
-If you prefer your inference rule on a separate line, maybe with a name,
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}} {\sc conjI}
-\end{center}
-is produced by
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
-\verb!\end{center}!
-\end{quote}
-It is not recommended to use the standard \texttt{display} option
-together with \texttt{Rule} because centering does not work and because
-the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
-clash.
-
-Of course you can display multiple rules in this fashion:
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
-\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
-\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
-\verb!\end{center}!
-\end{quote}
-yields
-\begin{center}\small
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}} {\sc conjI} \\[1ex]
-\isa{\mbox{}\inferrule{\mbox{P}}{\mbox{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}}} {\sc disjI$_1$} \qquad
-\isa{\mbox{}\inferrule{\mbox{Q}}{\mbox{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}}} {\sc disjI$_2$}
-\end{center}
-
-The \texttt{mathpartir} package copes well if there are too many
-premises for one line:
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B}\\\ \mbox{B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C}\\\ \mbox{C\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ D}\\\ \mbox{D\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ E}\\\ \mbox{E\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ F}\\\ \mbox{F\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ G}\\\ \mbox{G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ H}\\\ \mbox{H\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ I}\\\ \mbox{I\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ J}\\\ \mbox{J\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ K}}{\mbox{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ K}}}
-\end{center}
-
-Limitations: 1. Premises and conclusion must each not be longer than
-the line. 2. Premises that are \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}-implications are again
-displayed with a horizontal line, which looks at least unusual.
-
-
-In case you print theorems without premises no rule will be printed by the
-\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
-\verb!\end{center}!
-\end{quote}
-yields
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{}}{\mbox{t\ {\isaliteral{3D}{\isacharequal}}\ t}}} {\sc refl}
-\end{center}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Displays and font sizes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-When displaying theorems with the \texttt{display} option, e.g.
-\verb!@!\verb!{thm[display] refl}! \begin{isabelle}%
-t\ {\isaliteral{3D}{\isacharequal}}\ t%
-\end{isabelle} the theorem is
-set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
-which is also the style that regular theory text is set in, e.g.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent Otherwise \verb!\isastyleminor! is used,
-which does not modify the font size (assuming you stick to the default
-\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
-normal font size throughout your text, include
-\begin{quote}
-\verb!\renewcommand{\isastyle}{\isastyleminor}!
-\end{quote}
-in \texttt{root.tex}. On the other hand, if you like the small font,
-just put \verb!\isastyle! in front of the text in question,
-e.g.\ at the start of one of the center-environments above.
-
-The advantage of the display option is that you can display a whole
-list of theorems in one go. For example,
-\verb!@!\verb!{thm[display] append.simps}!
-generates \begin{isabelle}%
-{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isacharat\ ys\ {\isaliteral{3D}{\isacharequal}}\ ys\isasep\isanewline%
-x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys%
-\end{isabelle}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{If-then%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you prefer a fake ``natural language'' style you can produce
-the body of
-\newtheorem{theorem}{Theorem}
-\begin{theorem}
-\isa{{\normalsize{}If\,}\ \mbox{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ j}\ {\normalsize \,and\,}\ \mbox{j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k}\ {\normalsize \,then\,}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{2E}{\isachardot}}}
-\end{theorem}
-by typing
-\begin{quote}
-\verb!@!\verb!{thm[mode=IfThen] le_trans}!
-\end{quote}
-
-In order to prevent odd line breaks, the premises are put into boxes.
-At times this is too drastic:
-\begin{theorem}
-\isa{{\normalsize{}If\,}\ \mbox{longpremise}\ {\normalsize \,and\,}\ \mbox{longerpremise}\ {\normalsize \,and\,}\ \mbox{P\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}\ {\normalsize \,and\,}\ \mbox{longestpremise}\ {\normalsize \,then\,}\ conclusion{\isaliteral{2E}{\isachardot}}}
-\end{theorem}
-In which case you should use \texttt{IfThenNoBox} instead of
-\texttt{IfThen}:
-\begin{theorem}
-\isa{{\normalsize{}If\,}\ longpremise\ {\normalsize \,and\,}\ longerpremise\ {\normalsize \,and\,}\ P\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\normalsize \,and\,}\ longestpremise\ {\normalsize \,then\,}\ conclusion{\isaliteral{2E}{\isachardot}}}
-\end{theorem}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Doing it yourself\label{sec:yourself}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If for some reason you want or need to present theorems your
-own way, you can extract the premises and the conclusion explicitly
-and combine them as you like:
-\begin{itemize}
-\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
-prints premise 1 of $thm$.
-\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
-prints the conclusion of $thm$.
-\end{itemize}
-For example, ``from \isa{Q} and
-\isa{P} we conclude \isa{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}''
-is produced by
-\begin{quote}
-\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
-\end{quote}
-Thus you can rearrange or hide premises and typeset the theorem as you like.
-Styles like \verb!(prem 1)! are a general mechanism explained
-in \S\ref{sec:styles}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Patterns%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In \S\ref{sec:varnames} we shows how to create patterns containing
- ``\isa{\_}''.
- You can drive this game even further and extend the syntax of let
- bindings such that certain functions like \isa{fst}, \isa{hd},
- etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
- following:
-
- \begin{center}
- \begin{tabular}{l@ {~~produced by~~}l}
- \isa{\textsf{let}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ \_{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = fst p in t"}!\\
- \isa{\textsf{let}\ {\isaliteral{28}{\isacharparenleft}}\_{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = snd p in t"}!\\
- \isa{\textsf{let}\ x{\isaliteral{5C3C63646F743E}{\isasymcdot}}\_\ {\isaliteral{3D}{\isacharequal}}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
- \isa{\textsf{let}\ \_{\isaliteral{5C3C63646F743E}{\isasymcdot}}x\ {\isaliteral{3D}{\isacharequal}}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
- \isa{\textsf{let}\ Some\ x\ {\isaliteral{3D}{\isacharequal}}\ y\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = the y in t"}!\\
- \end{tabular}
- \end{center}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Proofs%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Full proofs, even if written in beautiful Isar style, are
-likely to be too long and detailed to be included in conference
-papers, but some key lemmas might be of interest.
-It is usually easiest to put them in figures like the one in Fig.\
-\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{figure}
- \begin{center}\begin{minipage}{0.6\textwidth}
- \isastyleminor\isamarkuptrue
-\isacommand{lemma}\isamarkupfalse%
-\ True\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{2D}{\isacharminus}}\isanewline
-\ \ %
-\isamarkupcmt{pretty trivial%
-}
-\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ True\ \isacommand{by}\isamarkupfalse%
-\ force\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\end{minipage}\end{center}
- \caption{Example proof in a figure.}\label{fig:proof}
- \end{figure}
-%
-\begin{isamarkuptext}%
-\begin{quote}
-\small
-\verb!text_raw {!\verb!*!\\
-\verb! \begin{figure}!\\
-\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
-\verb! \isastyleminor\isamarkuptrue!\\
-\verb!*!\verb!}!\\
-\verb!lemma True!\\
-\verb!proof -!\\
-\verb! -- "pretty trivial"!\\
-\verb! show True by force!\\
-\verb!qed!\\
-\verb!text_raw {!\verb!*!\\
-\verb! \end{minipage}\end{center}!\\
-\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
-\verb! \end{figure}!\\
-\verb!*!\verb!}!
-\end{quote}
-
-Other theory text, e.g.\ definitions, can be put in figures, too.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Styles\label{sec:styles}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \verb!thm! antiquotation works nicely for single theorems, but
- sets of equations as used in definitions are more difficult to
- typeset nicely: people tend to prefer aligned \isa{{\isaliteral{3D}{\isacharequal}}} signs.
-
- To deal with such cases where it is desirable to dive into the structure
- of terms and theorems, Isabelle offers antiquotations featuring
- ``styles'':
-
- \begin{quote}
- \verb!@!\verb!{thm (style) thm}!\\
- \verb!@!\verb!{prop (style) thm}!\\
- \verb!@!\verb!{term (style) term}!\\
- \verb!@!\verb!{term_type (style) term}!\\
- \verb!@!\verb!{typeof (style) term}!\\
- \end{quote}
-
- A ``style'' is a transformation of a term. There are predefined
- styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
- For example,
- the output
- \begin{center}
- \begin{tabular}{l@ {~~\isa{{\isaliteral{3D}{\isacharequal}}}~~}l}
- \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isacharat\ ys} & \isa{ys}\\
- \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys} & \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys}
- \end{tabular}
- \end{center}
- is produced by the following code:
- \begin{quote}
- \verb!\begin{center}!\\
- \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
- \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
- \verb!\end{tabular}!\\
- \verb!\end{center}!
- \end{quote}
- Note the space between \verb!@! and \verb!{! in the tabular argument.
- It prevents Isabelle from interpreting \verb!@ {~~...~~}!
- as an antiquotation. The styles \verb!lhs! and \verb!rhs!
- extract the left hand side (or right hand side respectively) from the
- conclusion of propositions consisting of a binary operator
- (e.~g.~\isa{{\isaliteral{3D}{\isacharequal}}}, \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}, \isa{{\isaliteral{3C}{\isacharless}}}).
-
- 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{xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd\ xs{\isaliteral{5C3C63646F743E}{\isasymcdot}}tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}
- \end{center}
- To print just the conclusion,
- \begin{center}
- \isa{hd\ xs{\isaliteral{5C3C63646F743E}{\isasymcdot}}tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}
- \end{center}
- type
- \begin{quote}
- \verb!\begin{center}!\\
- \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
- \verb!\end{center}!
- \end{quote}
- Beware that any options must be placed \emph{before}
- the style, as in this example.
-
- Further use cases can be found in \S\ref{sec:yourself}.
- If you are not afraid of ML, you may also define your own styles.
- Have a look at module \verb|Term_Style|.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/LaTeXsugar/Sugar/document/mathpartir.sty Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,388 +0,0 @@
-% Mathpartir --- Math Paragraph for Typesetting Inference Rules
-%
-% Copyright (C) 2001, 2002, 2003 Didier Rémy
-%
-% Author : Didier Remy
-% Version : 1.1.1
-% Bug Reports : to author
-% Web Site : http://pauillac.inria.fr/~remy/latex/
-%
-% WhizzyTeX is free software; you can redistribute it and/or modify
-% it under the terms of the GNU General Public License as published by
-% the Free Software Foundation; either version 2, or (at your option)
-% any later version.
-%
-% Mathpartir is distributed in the hope that it will be useful,
-% but WITHOUT ANY WARRANTY; without even the implied warranty of
-% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-% GNU General Public License for more details
-% (http://pauillac.inria.fr/~remy/license/GPL).
-%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% File mathpartir.sty (LaTeX macros)
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
- [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-\newdimen \mpr@tmpdim
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing
-% in mathpar or in inferrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
- \edef \MathparNormalpar
- {\noexpand \lineskiplimit \the\lineskiplimit
- \noexpand \lineskip \the\lineskip}%
- }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
- {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
- \let \and \mpr@andcr
- \let \par \mpr@andcr
- \let \\\mpr@cr
- \let \eqno \mpr@eqno
- \let \hva \mpr@hva
- }
-\let \MathparBindings \mpr@bindings
-
-% \@ifundefined {ignorespacesafterend}
-% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
-
-\newenvironment{mathpar}[1][]
- {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
- \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
- \noindent $\displaystyle\fi
- \MathparBindings}
- {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
- \vbox \bgroup \tabskip 0em \let \\ \cr
- \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
- \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
- \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
- \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
- \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
- \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
- \mpr@flatten \mpr@all \mpr@to \mpr@one
- \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
- \mpr@all \mpr@stripend
- \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
- \ifx 1\mpr@isempty
- \repeat
-}
-
-%% Part III -- Type inference rules
-
-\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
- \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@htovlist {%
- \setbox \mpr@hlist
- \hbox {\strut
- \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
- \unhbox \mpr@hlist}%
- \setbox \mpr@vlist
- \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
- \else \unvbox \mpr@vlist \box \mpr@hlist
- \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-% \setbox \mpr@hlist
-% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-% \setbox \mpr@vlist
-% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
-% \else \unvbox \mpr@vlist \box \mpr@hlist
-% \fi}%
-% }
-
-\def \mpr@sep{2em}
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
- \bgroup
- \ifx #1T\@premissetrue
- \else \ifx #1B\@premissefalse
- \else
- \PackageError{mathpartir}
- {Premisse orientation should either be P or B}
- {Fatal error in Package}%
- \fi \fi
- \def \@test {#2}\ifx \@test \mpr@blank\else
- \setbox \mpr@hlist \hbox {}%
- \setbox \mpr@vlist \vbox {}%
- \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
- \let \@hvlist \empty \let \@rev \empty
- \mpr@tmpdim 0em
- \expandafter \mpr@makelist #2\mpr@to \mpr@flat
- \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
- \def \\##1{%
- \def \@test {##1}\ifx \@test \empty
- \mpr@htovlist
- \mpr@tmpdim 0em %%% last bug fix not extensively checked
- \else
- \setbox0 \hbox{$\displaystyle {##1}$}\relax
- \advance \mpr@tmpdim by \wd0
- %\mpr@tmpdim 1.02\mpr@tmpdim
- \ifnum \mpr@tmpdim < \hsize
- \ifnum \wd\mpr@hlist > 0
- \if@premisse
- \setbox \mpr@hlist
- \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
- \else
- \setbox \mpr@hlist
- \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
- \fi
- \else
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \else
- \ifnum \wd \mpr@hlist > 0
- \mpr@htovlist
- \mpr@tmpdim \wd0
- \fi
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \advance \mpr@tmpdim by \mpr@sep
- \fi
- }%
- \@rev
- \mpr@htovlist
- \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
- \fi
- \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
- \let\@@over\over % fallback if amsmath is not loaded
- \let\@@overwithdelims\overwithdelims
- \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
- \let\@@above\above \let\@@abovewithdelims\abovewithdelims
- }{}
-
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
- $\displaystyle {#1\@@over #2}$}}
-\let \mpr@fraction \mpr@@fraction
-\def \mpr@@reduce #1#2{\hbox
- {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@@rewrite #1#2#3{\hbox
- {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
- {\bgroup
- \ifnum \linewidth<\hsize \hsize \linewidth\fi
- \mpr@rulelineskip
- \let \and \qquad
- \let \hva \mpr@hva
- \let \@rulename \mpr@empty
- \let \@rule@options \mpr@empty
- \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
- {\everymath={\displaystyle}%
- \def \@test {#2}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
- \else
- \def \@test {#3}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
- \else
- \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
- \fi \fi
- \def \@test {#1}\ifx \@test\empty \box0
- \else \vbox
-%%% Suggestion de Francois pour les etiquettes longues
-%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
- {\hbox {\RefTirName {#1}}\box0}\fi
- \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \inferrule [label]{[premisses}{conclusions}
-% or
-% \inferrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible,
-% and vertical breaks if needed.
-%
-% An empty element obtained by \\\\ produces a vertical break in all cases.
-%
-% The former rule is aligned on the fraction bar.
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-%
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%
-% width set the width of the rule to val
-% narrower set the width of the rule to val\hsize
-% before execute val at the beginning/left
-% lab put a label [Val] on top of the rule
-% lskip add negative skip on the right
-% left put a left label [Val]
-% Left put a left label [Val], ignoring its width
-% right put a right label [Val]
-% Right put a right label [Val], ignoring its width
-% leftskip skip negative space on the left-hand side
-% rightskip skip negative space on the right-hand side
-% vdots lift the rule by val and fill vertical space with dots
-% after execute val at the end/right
-%
-% Note that most options must come in this order to avoid strange
-% typesetting (in particular leftskip must preceed left and Left and
-% rightskip must follow Right or right; vdots must come last
-% or be only followed by rightskip.
-%
-
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\def \mprset #1{\setkeys{mprset}{#1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{sep}{\def\mpr@sep{#1}}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
-\define@key {mpr}{right}
- {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
- \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{RIGHT}
- {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
- \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-
-\newdimen \rule@dimen
-\newcommand \mpr@inferstar@ [3][]{\setbox0
- \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
- \setbox \mpr@right \hbox{}%
- $\setkeys{mpr}{#1}%
- \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
- \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
- \box \mpr@right \mpr@vdots$}
- \setbox1 \hbox {\strut}
- \rule@dimen \dp0 \advance \rule@dimen by -\dp1
- \raise \rule@dimen \box0}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode
- \let \@do \mpr@inferstar@
- \else
- \let \@do \mpr@err@skipargs
- \PackageError {mathpartir}
- {\string\inferrule* can only be used in math mode}{}%
- \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \tir@name #1{\hbox {\small \sc #1}}
-\let \TirName \tir@name
-\let \RefTirName \tir@name
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-
-
-\endinput
--- a/doc-src/LaTeXsugar/Sugar/document/root.bib Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
-title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
-publisher=Springer,series=LNCS,volume=2283,year=2002,
-note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
-
-@misc{mathpartir,author={Didier R\'emy},title={mathpartir},
-note={\url{http://cristal.inria.fr/~remy/latex/}}}
-
-@misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow},
-title={{LaTeX} sugar theories and support files},
-note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}}
-
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{../../../../lib/texinputs/isabelle,../../../../lib/texinputs/isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-% use only when needed
-\usepackage{amssymb}
-
-\usepackage{mathpartir}
-
-% this should be the last package used
-\usepackage{../../../pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-\hyphenation{Isa-belle}
-\begin{document}
-
-\title{\LaTeX\ Sugar for Isabelle Documents}
-\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
-\maketitle
-
-\begin{abstract}
-This document shows how to typset mathematics in Isabelle-based
-documents in a style close to that in ordinary computer science papers.
-\end{abstract}
-
-%\tableofcontents
-
-% generated text of all theories
-\input{Sugar.tex}
-
-% optional bibliography
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/document/build Mon Aug 27 22:22:42 2012 +0200
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+"$ISABELLE_TOOL" latex -o sty
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o bbl
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_HOME/doc-src/sedindex" root
+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/document/mathpartir.sty Mon Aug 27 22:22:42 2012 +0200
@@ -0,0 +1,388 @@
+% Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+% Copyright (C) 2001, 2002, 2003 Didier Rémy
+%
+% Author : Didier Remy
+% Version : 1.1.1
+% Bug Reports : to author
+% Web Site : http://pauillac.inria.fr/~remy/latex/
+%
+% WhizzyTeX is free software; you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either version 2, or (at your option)
+% any later version.
+%
+% Mathpartir is distributed in the hope that it will be useful,
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details
+% (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+ [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+\newdimen \mpr@tmpdim
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+ \edef \MathparNormalpar
+ {\noexpand \lineskiplimit \the\lineskiplimit
+ \noexpand \lineskip \the\lineskip}%
+ }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+ {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+ \let \and \mpr@andcr
+ \let \par \mpr@andcr
+ \let \\\mpr@cr
+ \let \eqno \mpr@eqno
+ \let \hva \mpr@hva
+ }
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+ {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+ \noindent $\displaystyle\fi
+ \MathparBindings}
+ {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
+ \vbox \bgroup \tabskip 0em \let \\ \cr
+ \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+ \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+ \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+ \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+ \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
+ \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+ \mpr@flatten \mpr@all \mpr@to \mpr@one
+ \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+ \mpr@all \mpr@stripend
+ \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+ \ifx 1\mpr@isempty
+ \repeat
+}
+
+%% Part III -- Type inference rules
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+ \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+ \setbox \mpr@hlist
+ \hbox {\strut
+ \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+ \unhbox \mpr@hlist}%
+ \setbox \mpr@vlist
+ \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+ \else \unvbox \mpr@vlist \box \mpr@hlist
+ \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+% \setbox \mpr@hlist
+% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+% \setbox \mpr@vlist
+% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+% \else \unvbox \mpr@vlist \box \mpr@hlist
+% \fi}%
+% }
+
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+ \bgroup
+ \ifx #1T\@premissetrue
+ \else \ifx #1B\@premissefalse
+ \else
+ \PackageError{mathpartir}
+ {Premisse orientation should either be P or B}
+ {Fatal error in Package}%
+ \fi \fi
+ \def \@test {#2}\ifx \@test \mpr@blank\else
+ \setbox \mpr@hlist \hbox {}%
+ \setbox \mpr@vlist \vbox {}%
+ \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+ \let \@hvlist \empty \let \@rev \empty
+ \mpr@tmpdim 0em
+ \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+ \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+ \def \\##1{%
+ \def \@test {##1}\ifx \@test \empty
+ \mpr@htovlist
+ \mpr@tmpdim 0em %%% last bug fix not extensively checked
+ \else
+ \setbox0 \hbox{$\displaystyle {##1}$}\relax
+ \advance \mpr@tmpdim by \wd0
+ %\mpr@tmpdim 1.02\mpr@tmpdim
+ \ifnum \mpr@tmpdim < \hsize
+ \ifnum \wd\mpr@hlist > 0
+ \if@premisse
+ \setbox \mpr@hlist
+ \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+ \else
+ \setbox \mpr@hlist
+ \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
+ \fi
+ \else
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \else
+ \ifnum \wd \mpr@hlist > 0
+ \mpr@htovlist
+ \mpr@tmpdim \wd0
+ \fi
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \advance \mpr@tmpdim by \mpr@sep
+ \fi
+ }%
+ \@rev
+ \mpr@htovlist
+ \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+ \fi
+ \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+ \let\@@over\over % fallback if amsmath is not loaded
+ \let\@@overwithdelims\overwithdelims
+ \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+ \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+ }{}
+
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\@@over #2}$}}
+\let \mpr@fraction \mpr@@fraction
+\def \mpr@@reduce #1#2{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+ {\bgroup
+ \ifnum \linewidth<\hsize \hsize \linewidth\fi
+ \mpr@rulelineskip
+ \let \and \qquad
+ \let \hva \mpr@hva
+ \let \@rulename \mpr@empty
+ \let \@rule@options \mpr@empty
+ \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+ {\everymath={\displaystyle}%
+ \def \@test {#2}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+ \else
+ \def \@test {#3}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+ \else
+ \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+ \fi \fi
+ \def \@test {#1}\ifx \@test\empty \box0
+ \else \vbox
+%%% Suggestion de Francois pour les etiquettes longues
+%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+ {\hbox {\RefTirName {#1}}\box0}\fi
+ \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \\
+% Each \\ produces a break, attempting horizontal breaks if possible,
+% and vertical breaks if needed.
+%
+% An empty element obtained by \\\\ produces a vertical break in all cases.
+%
+% The former rule is aligned on the fraction bar.
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+%
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%
+% width set the width of the rule to val
+% narrower set the width of the rule to val\hsize
+% before execute val at the beginning/left
+% lab put a label [Val] on top of the rule
+% lskip add negative skip on the right
+% left put a left label [Val]
+% Left put a left label [Val], ignoring its width
+% right put a right label [Val]
+% Right put a right label [Val], ignoring its width
+% leftskip skip negative space on the left-hand side
+% rightskip skip negative space on the right-hand side
+% vdots lift the rule by val and fill vertical space with dots
+% after execute val at the end/right
+%
+% Note that most options must come in this order to avoid strange
+% typesetting (in particular leftskip must preceed left and Left and
+% rightskip must follow Right or right; vdots must come last
+% or be only followed by rightskip.
+%
+
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\def \mprset #1{\setkeys{mprset}{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+ {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+ {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newdimen \rule@dimen
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+ \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+ \setbox \mpr@right \hbox{}%
+ $\setkeys{mpr}{#1}%
+ \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+ \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+ \box \mpr@right \mpr@vdots$}
+ \setbox1 \hbox {\strut}
+ \rule@dimen \dp0 \advance \rule@dimen by -\dp1
+ \raise \rule@dimen \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode
+ \let \@do \mpr@inferstar@
+ \else
+ \let \@do \mpr@err@skipargs
+ \PackageError {mathpartir}
+ {\string\inferrule* can only be used in math mode}{}%
+ \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \tir@name #1{\hbox {\small \sc #1}}
+\let \TirName \tir@name
+\let \RefTirName \tir@name
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/document/root.bib Mon Aug 27 22:22:42 2012 +0200
@@ -0,0 +1,12 @@
+@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
+title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
+publisher=Springer,series=LNCS,volume=2283,year=2002,
+note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
+
+@misc{mathpartir,author={Didier R\'emy},title={mathpartir},
+note={\url{http://cristal.inria.fr/~remy/latex/}}}
+
+@misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow},
+title={{LaTeX} sugar theories and support files},
+note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/document/root.tex Mon Aug 27 22:22:42 2012 +0200
@@ -0,0 +1,43 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also isabellesym.sty)
+% use only when needed
+\usepackage{amssymb}
+
+\usepackage{mathpartir}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+\hyphenation{Isa-belle}
+\begin{document}
+
+\title{\LaTeX\ Sugar for Isabelle Documents}
+\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
+\maketitle
+
+\begin{abstract}
+This document shows how to typset mathematics in Isabelle-based
+documents in a style close to that in ordinary computer science papers.
+\end{abstract}
+
+%\tableofcontents
+
+% generated text of all theories
+\input{Sugar.tex}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- a/doc-src/ROOT Mon Aug 27 22:14:17 2012 +0200
+++ b/doc-src/ROOT Mon Aug 27 22:22:42 2012 +0200
@@ -103,13 +103,17 @@
quick_and_dirty]
theories ZF_Specific
-session LaTeXsugar (doc) in "LaTeXsugar/Sugar" = HOL +
- options [browser_info = false, document = false,
- document_dump = document, document_dump_mode = "tex"]
- theories [document_dump = ""]
+session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
+ options [document_variants = "sugar"]
+ theories [document = ""]
"~~/src/HOL/Library/LaTeXsugar"
"~~/src/HOL/Library/OptionalSugar"
theories Sugar
+ files
+ "document/build"
+ "document/mathpartir.sty"
+ "document/root.bib"
+ "document/root.tex"
session Locales (doc) in "Locales" = HOL +
options [document_variants = "locales"]