--- a/doc-src/LaTeXsugar/Makefile Tue Jun 14 23:44:37 2005 +0200
+++ b/doc-src/LaTeXsugar/Makefile Wed Jun 15 09:01:15 2005 +0200
@@ -17,8 +17,8 @@
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/mathpartir.sty Sugar/document/LaTeXsugar.tex \
+ Sugar/document/OptionalSugar.tex Sugar/document/Sugar.tex
GARBAGE = Sugar/document/*.aux Sugar/document/*.log Sugar/document/*.toc \
Sugar/document/*.idx Sugar/document/*.bbl Sugar/document/*.blg \
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue Jun 14 23:44:37 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Jun 15 09:01:15 2005 +0200
@@ -128,6 +128,23 @@
(*<*)ML"reset show_question_marks"(*>*)
+subsection "Variable names"
+
+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}
+*}
+
subsection "Inference rules"
text{* To print theorems as inference rules you need to include Didier