%  Locallabel
%
%  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/
% 
%  Locallabel 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.
%  
%  Locallabel 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 locallabel.tex (LaTeX macros)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass{article}
\usepackage{locallabel}
\title {Local labels}
\author {Didier R{\'{e}}my}

\begin{document}
\maketitle

\begin{abstract}
This package provides macros to generate numeric references and refer to
them by name, much as equation numbers, except that numbers and names can be
reset at any time. One typical use is to refer to facts beeing establish
during a proof until completion of the proof and be able to do so in the
next proof without any clash of names of labels. 

The package also comes with a version for {HeVeA}.
\end{abstract}

%HEVEA \def \basis {http://cristal.inria.fr/\home{remy}/latex}
%HEVEA This document is also available in
%HEVEA \ahref {\basis/locallabel.dvi}{DVI}, 
%HEVEA \ahref {\basis/locallabel.ps.gz}{Postscript}, and
%HEVEA \ahref {\basis/locallabel.pdf}{PDF}.
%HEVEA 
%HEVEA The source of this file,
%HEVEA \ahref {\basis/locallabel.tex}{locallabel.tex}
%HEVEA may serve as an example.

\section {Example}

\newtheorem{theorem}{Theorem}{}{}
\newenvironment{proof}{\begin{quote}\underline{Proof: }}{\end{quote}}

\begin{theorem}
\label{socrate-mortal}
Socrate is mortal.
\end{theorem}
\begin{proof}
Socrate is a man~\llabel[sm-one]{sm}.
It is well-known that all man are mortal~\llabel{mm}.
Hence, by~\lref {sm} and \lref {mm}, Socrate is mortal.
\end{proof}
Let me prove it another way:
\begin{proof}
\locallabelreset
It is well-known that all man are mortal~\llabel{mm}.
Socrate is a man~\llabel[sm-two]{sm}.
Hence, by~\lref {mm} and \lref {sm}, Socrate is mortal.
\end{proof}
Did you notice that fact \LrefTypeset{\ref{sm-one}} of first proof
became fact \LrefTypeset{\ref{sm-two}} in the second proof?

\section {Short manual}

\def \arg#1{\{\noarg{#1}\}}
\def \noarg #1{$\langle\textsc{#1}\rangle$}
\noindent
\texttt{\string\locallabelreset}
\begin{quote}
Reset numeric labels and names to refer to them
\end{quote}
\texttt{\string\llabel}\arg{Name}
\begin{quote}
Creates a new numeric label, binds it to \noarg{Name}, 
and print the label as a binding occurrence. 

This primitive may take a \noarg{Gname} as optional argument, so that the
\texttt{\string\ref}\arg{Gname} can be used to refer to this label in any
context. Of course \noarg{Gname} is subject to overriding and name clashes
exactly as all global labels do.
\end{quote}
\texttt{\string\lref}\arg{Name}
\begin{quote}
Prints numeric use occurrence of label \noarg{Name}.
\end{quote}
\texttt{\string\lbind}\arg{Name}
\begin{quote}
This creates the label as \texttt{\string\llabel}, but does not print it. 
This can be used to skip one numeric value or to assign them in a controlled
order. In this case, the next use of \texttt{\string\llabel}\arg{Name}
will print the name of the label as a binding occurrence. 

If \texttt{\string\llabel}\arg{Name} is repeated with the same name
\noarg{Name} a warning will be issued.
\end{quote}

\paragraph{Customization}

You may redefined the followuing macros to change the appearance of binding
and use occurrences: \par \medskip\noindent
\texttt{\string\LlabelTypeset\arg{Val}}
\begin{quote}
Typesets \noarg {Val} as a binding occurrence.
\end{quote}
\texttt{\string\LrefTypeset\arg{Val}}
\begin{quote}
Typesets \noarg {Val} as a use occurrence.
\end{quote}

\section {Code of the example}

\begin{quote}
\small
\begin{verbatim}
\begin{theorem}\label{socrate-mortal}Socrate is mortal.
\end{theorem}
\begin{proof}
Socrate is a man~\llabel[socrate-man]{sm}.  It is well-known that all man
are mortal~\llabel{mm}.  Hence, by~\lref {sm} and \lref {mm}, Socrate is
mortal.
\end{proof}
Did you hear what I said?
\begin{theorem}
Socrate is mortal.
\end{theorem}
Let me prove it another way:
\begin{proof}
\locallabelreset
It is well-known that all man are mortal~\llabel{mm}.  Socrate is a
man~\llabel {sm}.  Hence, by~\lref {mm} and \lref {sm}, Socrate is mortal.
\end{proof}
Actually, in the proof of Theorem~\ref{socrate-mortal}, 
claim \ref{socrate-man} is arguable.
\end{verbatim}
\end{quote}


\end{document}