# HG changeset patch
# User nipkow
# Date 1118818875 -7200
# Node ID 3446d2b6a19f3b1873278e54d9312475a697105f
# Parent  495dbcd4f4c907a61e37e062ce046a8a799e154d
documented DUMMY

diff -r 495dbcd4f4c9 -r 3446d2b6a19f doc-src/LaTeXsugar/Makefile
--- 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 \
diff -r 495dbcd4f4c9 -r 3446d2b6a19f doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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