# HG changeset patch # User wenzelm # Date 962311149 -7200 # Node ID 738056d60a2afb4ba0cf81358735fa213fd52a6f # Parent 435fef035d7f10f4f97edfccdbf04afb8da7cabb added \indexisarant; diff -r 435fef035d7f -r 738056d60a2a doc-src/isar.sty --- a/doc-src/isar.sty Thu Jun 29 22:38:30 2000 +0200 +++ b/doc-src/isar.sty Thu Jun 29 22:39:09 2000 +0200 @@ -16,6 +16,7 @@ \newcommand{\indexisarthm}[1]{\index{#1 (theorem)|bold}\index{Theorems!#1|bold}} \newcommand{\indexisarvar}[1]{\index{#1 (variable)|bold}\index{Variables!#1|bold}} \newcommand{\indexisarcase}[1]{\index{#1 (case)|bold}\index{Cases!#1|bold}} +\newcommand{\indexisarant}[1]{\index{#1 (antiquotation)|bold}\index{Antiquotations!#1|bold}} \newcommand{\isarcmd}[1]{\isarkeyword{#1}} \newcommand{\isartrans}[2]{#1 \mathbin{\,\to\,} #2}