[ProofPower] Confused about Z and HOL terms

[Marcel Oliveira]

Hi everybody,

Please take a look in the attached document.

First: I couldn't understand why the output for the hol_term_1 is between Z
quotations, as it were a Z term. Does anyone know why?

Second: In hol_term_2, I am trying to declare a HOL predicate as the desired
output presented in the document. However, of course I cannot apply mk_(not)
to the pre sch. I've bee trying very hard to get the desired predicate but,
until now, couldn't find a way. Does any one know how to do it? (note that,
if possible, I would like a pure HOL term, with no Z terms inside it.)

Thanks a lot,

Marcel

P.S.: Sorry for the confusin in the att. When I was trying to convert it to
ascii it gave me an error message. For this reason i am sending the original
(extended) doc, the generated (ascii) asc, and a dvi just in case.

===============================
Marcel Oliveira
PhD Researcher - Circus Project
Formal Methods
Computing Laboratory
University of Kent
Canterbury, Kent, UK  CT2 7NF
Tel: 44 (0)1227 823192
E-Mail: mvmo2 at kent.ac.uk
===============================
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test-email.doc
Type: application/msword
Size: 756 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040513/e54297f0/attachment.doc>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test-email.asc
Type: application/octet-stream
Size: 921 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040513/e54297f0/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test-email.dvi
Type: application/octet-stream
Size: 3136 bytes
Desc: not available
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040513/e54297f0/attachment-0001.obj>