# Re: [ProofPower] Broken theory indexes

On Tuesday 10 Aug 2010 15:17, you wrote:
> On 9 Aug 2010, at 19:20, Roger Bishop Jones wrote:
> > ...The failure was connected with my trying (and
> > failing) to redefine something defined in
> > ProofPower.sty (instead of having my own special
> > version of it).
> > Does anyone know a way to override a definition in a
> > style file (other than by editing it)?
>
> What kind of definition are you trying to override?

The following definition:

\def\holindexon{\def\holin...@aux##1{%
\suppr...@quotechars
\MMM{\def\${\noexpand\$}
\edef\Temp{##1}\index{\Temp }}}}

The last line of which I changed to:

\edef\Temp{##1}\index{!\Temp }}}}

I did this in a file called rbj.sty, which is as follows:

\typeout{$Id: rbj.sty,v 1.2 2010-08-08 15:50:44 rbj Exp$}
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{rbj}
\RequirePackage{ProofPower}
\RequirePackage{mathabx}
\def\Zdef{\MMM{\corresponds}}
\def\holindexon{\def\holin...@aux##1{%
\suppr...@quotechars
\MMM{\def\${\noexpand\$}
\edef\Temp{##1}\index{!\Temp }}}}

I then invoked package rbj instead of ProoFPower in my
ProofPower .doc file.

> For what TeX calls macros and LaTeX calls commands, the
> TeX \def or \let will override and existing definition
> while in LaTeX you have to use \renewcommand rather than
> \newcommand. For LaTeX environments, you use
> \renewenvironment. Do bear in that both TeX and LaTeX
> are block-structured, but LaTeX has something called
> \gdef which lets you make top-level definitions from
> within a block.

Unfortunately the distinction between tex and Latex
environments is one which I have not grasped, so I don't
know which I am in.  However, since ProofPower uses \def I
guess it must be in a tex environment, and so I would
suppose that my change is also.

Possibly my problem is that my redefinition comes later than
the crucial invocation of HOLindexOn.
I see that it is invoked immediately, so perhaps I should
reinvoke after my redefinition.

Roger Jones

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com