| changeset 20470 | c839b38a1f32 |
| parent 20451 | 27ea2ba48fa3 |
| child 20478 | de1bd9717d6c |
--- a/doc-src/IsarImplementation/style.sty Mon Sep 04 15:27:30 2006 +0200 +++ b/doc-src/IsarImplementation/style.sty Mon Sep 04 16:28:27 2006 +0200 @@ -7,6 +7,7 @@ %% references \newcommand{\secref}[1]{\S\ref{#1}} +\newcommand{\chref}[1]{chapter~\ref{#1}} \newcommand{\figref}[1]{figure~\ref{#1}} %% glossary