1.1 --- a/doc-src/LaTeXsugar/Makefile	Tue Jun 14 23:44:37 2005 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Makefile	Wed Jun 15 09:01:15 2005 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4  NAME = sugar
     1.5  
     1.6  FILES = Sugar/document/root.tex Sugar/document/root.bib \
     1.7 -	      Sugar/document/mathpartir.sty Sugar/document/LaTeXsugar.tex \
     1.8 -        Sugar/document/OptionalSugar.tex
     1.9 +        Sugar/document/mathpartir.sty Sugar/document/LaTeXsugar.tex \
    1.10 +        Sugar/document/OptionalSugar.tex Sugar/document/Sugar.tex
    1.11  
    1.12  GARBAGE = Sugar/document/*.aux Sugar/document/*.log Sugar/document/*.toc \
    1.13            Sugar/document/*.idx Sugar/document/*.bbl Sugar/document/*.blg \

     2.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue Jun 14 23:44:37 2005 +0200
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Jun 15 09:01:15 2005 +0200
     2.3 @@ -128,6 +128,23 @@
     2.4  
     2.5  (*<*)ML"reset show_question_marks"(*>*)
     2.6  
     2.7 +subsection "Variable names"
     2.8 +
     2.9 +text{* It sometimes happens that you want to change the name of a
    2.10 +variable in a theorem before printing it. This can easily be achieved
    2.11 +with the help of Isabelle's instantiation attribute \texttt{where}:
    2.12 +@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
    2.13 +\begin{quote}
    2.14 +\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
    2.15 +\end{quote}
    2.16 +To support the ``\_''-notation for irrelevant variables
    2.17 +the constant \texttt{DUMMY} has been introduced:
    2.18 +@{thm fst_conv[where b = DUMMY]} is produced by
    2.19 +\begin{quote}
    2.20 +\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
    2.21 +\end{quote}
    2.22 +*}
    2.23 +
    2.24  subsection "Inference rules"
    2.25  
    2.26  text{* To print theorems as inference rules you need to include Didier