Re: [ProofPower] Printing of \not\in
Rob,
I just made something like your document to exhibit the
problem and I see that it doesn't.
In a sample document exhibiting the problem I have:
\usepackage{latexsym}
\usepackage{rbj}
and rbj.sty has in it:
\RequirePackage{Proofpower}
\RequirePackage{mathabx}
However, adding these two font packages to the simplest
example does not create the problem.
I will get back to you when I have managed to reproduce the
problem in a minimal context.
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
Roger, > On Monday 11 Jul 2011 17:05, Rob Arthan wrote: > >> And presumably your docpdf calls pdflatex (which will >> fail in just the same way as texdvi on this example, I >> think you will find). So with this very simple example, >> the way ProofPower.sty does it works and the workaround >> you needed to get it working in your real example >> doesn't work. I think the next step has to be for you to >> try adding the style files you use to the simple example >> to see if we can figure out which one is causing the >> problem. > > I think it does, but the main differences are to do with > processing indexes, which may not be relevant to the problem > under discussion. > > Unfortunately I don't have a clue what is going on, i.e. I > still don't understand what the problem is. The problem is almost certainly that a style file you are using is redefining either \not and/or \notin and/or something that these macros depend on. > > If you would send me the test.doc file that might help me to > understand the problem you are addressing. I am trying to address your problem. The .doc file I was using is exactly like the .tex file but with =TEX at the beginning. I was just trying to suggest a quick way for you produce a minimal example of your problem, but any convenient way of getting a reasonably short .tex file that reproduces your problem will help. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
On Monday 11 Jul 2011 17:05, Rob Arthan wrote: > And presumably your docpdf calls pdflatex (which will > fail in just the same way as texdvi on this example, I > think you will find). So with this very simple example, > the way ProofPower.sty does it works and the workaround > you needed to get it working in your real example > doesn't work. I think the next step has to be for you to > try adding the style files you use to the simple example > to see if we can figure out which one is causing the > problem. I think it does, but the main differences are to do with processing indexes, which may not be relevant to the problem under discussion. Unfortunately I don't have a clue what is going on, i.e. I still don't understand what the problem is. If you would send me the test.doc file that might help me to understand the problem you are addressing. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
Roger,
On 10 Jul 2011, at 16:59, Roger Bishop Jones wrote:
> Rob,
>
> On Sunday 10 Jul 2011 15:59, you wrote:
>>
>> What happens if you just run doctex and then texdvi on
>> this file:
>>
>> http://dl.dropbox.com/u/34693999/ProofPower/rbj-not-in.te
>> x
>>
>> For me it fails on the second GFT section, when the
>> %notmem% character is expanded to \notin rather than
>> \not\in.
>
> You just asked me to run doctex on a tex file, so I skipped
> that step.
>
> When I ran texdvi I got:
>
> ! Illegal parameter number in definition of \Temp.
>
> \crcr
> l.14 ...ng \Backslash{}notin : \PrNL{}\PrIO{}\PrNN
> {}\\
>
>
> What I normally do is run "docpdf" which is my own lash up
> (using "makeindex").
>
And presumably your docpdf calls pdflatex (which will fail in just the same way
as texdvi on this example, I think you will find). So with this very simple
example, the way ProofPower.sty does it works and the workaround you needed to
get it working in your real example doesn't work. I think the next step has to
be for you to try adding the style files you use to the simple example to see
if we can figure out which one is causing the problem.
Regards,
Rob.
> Roger
>
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
Rob,
On Sunday 10 Jul 2011 15:59, you wrote:
>
> What happens if you just run doctex and then texdvi on
> this file:
>
> http://dl.dropbox.com/u/34693999/ProofPower/rbj-not-in.te
> x
>
> For me it fails on the second GFT section, when the
> %notmem% character is expanded to \notin rather than
> \not\in.
You just asked me to run doctex on a tex file, so I skipped
that step.
When I ran texdvi I got:
! Illegal parameter number in definition of \Temp.
\crcr
l.14 ...ng \Backslash{}notin : \PrNL{}\PrIO{}\PrNN
{}\\
What I normally do is run "docpdf" which is my own lash up
(using "makeindex").
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
Roger,
On 10 Jul 2011, at 14:08, Roger Bishop Jones wrote:
> On Sunday 10 Jul 2011 12:22, Rob Arthan wrote:
>> Roger,
>>
>> I had put this on my list of things to fix by changing
>> \not\in in the style file to \notin, but I get exactly
>> the opposite problem: \not\in work but \notin fails. Are
>> you still having this problem? I am suspecting that you
>> are using a style file that redefines both \not and
>> \notin to something different from what LaTeX gives you
>> out of the box. Note that \notin is not in the standard
>> list of mathematical symbols in the LaTeX User's Guide.
>
> I have the following in those of my documents which use the
> character:
>
> \def\PrIO{\MMM{\notin}}
>
> I don't understand how you get the opposite problem.
>
What happens if you just run doctex and then texdvi on this file:
http://dl.dropbox.com/u/34693999/ProofPower/rbj-not-in.tex
For me it fails on the second GFT section, when the %notmem% character is
expanded to \notin rather than \not\in.
Regards,
Rob.
> Roger
>
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
On Sunday 10 Jul 2011 12:22, Rob Arthan wrote:
> Roger,
>
> I had put this on my list of things to fix by changing
> \not\in in the style file to \notin, but I get exactly
> the opposite problem: \not\in work but \notin fails. Are
> you still having this problem? I am suspecting that you
> are using a style file that redefines both \not and
> \notin to something different from what LaTeX gives you
> out of the box. Note that \notin is not in the standard
> list of mathematical symbols in the LaTeX User's Guide.
I have the following in those of my documents which use the
character:
\def\PrIO{\MMM{\notin}}
I don't understand how you get the opposite problem.
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
Roger,
I had put this on my list of things to fix by changing \not\in in the style
file to \notin, but I get exactly the opposite problem: \not\in work but \notin
fails. Are you still having this problem? I am suspecting that you are using a
style file that redefines both \not and \notin to something different from what
LaTeX gives you out of the box. Note that \notin is not in the standard list of
mathematical symbols in the LaTeX User's Guide.
Regards,
Rob.
On 31 Mar 2011, at 14:26, Roger Bishop Jones wrote:
> On Tuesday 29 Mar 2011 16:48, Rob Arthan wrote:
>
>> It works fine for me. What goes wrong?
>
> The failing occurrences are either in index brackets or in
> theory listings (probably also in index brackets).
>
> The actual error message is:
>
> ! Undefined control sequence.
> \not #1->\let \@@not
> =\not \let \@@n =\n \let \not =\relax
> \let \n =\relax \...
> l.849 ...M{} \$\PrNL{}\PrIO{}\PrIJ{m}\PrIJ{p}\PrNN
> {}: S
> \PrKN{} S \PrKN{} PR...
>
> Unfortunately I don't know how to read these things and
> hence don't know exactly what it is complaining about,
> but the odds are it is the double at signs.
>
> Also I should say that I am using hyperref and makeindex
> rather than the standard indexing arrangements, which I
> would be inclined to blame if the failure was in the index,
> but I don't see how it (makeindex) affects these occurrences.
>
> Roger
>
>
>
>
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
On Tuesday 29 Mar 2011 16:48, Rob Arthan wrote:
> It works fine for me. What goes wrong?
The failing occurrences are either in index brackets or in
theory listings (probably also in index brackets).
The actual error message is:
! Undefined control sequence.
\not #1->\let \@@not
=\not \let \@@n =\n \let \not =\relax
\let \n =\relax \...
l.849 ...M{} \$\PrNL{}\PrIO{}\PrIJ{m}\PrIJ{p}\PrNN
{}: S
\PrKN{} S \PrKN{} PR...
Unfortunately I don't know how to read these things and
hence don't know exactly what it is complaining about,
but the odds are it is the double at signs.
Also I should say that I am using hyperref and makeindex
rather than the standard indexing arrangements, which I
would be inclined to blame if the failure was in the index,
but I don't see how it (makeindex) affects these occurrences.
Roger
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Printing of \not\in
Roger,
It works fine for me. What goes wrong?
Regards,
Rob.
On 27 Mar 2011, at 11:50, Roger Bishop Jones wrote:
> I have used today (possibly for the first time) the not a
> member of symbol in ProofPower HOL and find that it causes an
> error in pdflatex.
>
> The definition in ProofPower.sty is:
>
> \def\PrIO{\MMM{\not\in}}
>
> which doesn't work (not in my environment), but:
>
> \def\PrIO{\MMM{\notin}}
>
> works fine.
>
> Roger Jones
>
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Printing of \not\in
I have used today (possibly for the first time) the not a
member of symbol in ProofPower HOL and find that it causes an
error in pdflatex.
The definition in ProofPower.sty is:
\def\PrIO{\MMM{\not\in}}
which doesn't work (not in my environment), but:
\def\PrIO{\MMM{\notin}}
works fine.
Roger Jones
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
