[ProofPower] Two questions

[Stephen Brackin]

Here's a dumb question: What's wrong with this?  spec_nth_asm_tac objects
that the relevant assumption isn't universally quantified, but it is.

%SZG%[ PT ]%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%%BHH%
%BV% p:PT
%EZ%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%

set_goal([],%SZT%{p} %neq% %emptyset%%>%);
a(rewrite_thm_tac (get_thm "z_sets" "z_%neq%_thm"));
a(rewrite_thm_tac (get_defn "z_sets" "%emptyset%"));
a(rewrite_thm_tac (get_thm "z_sets" "z_sets_ext_clauses"));
a(contr_tac);
a(spec_nth_asm_tac 1 %SZT%p%>%);

Here's a better question: Do you have any suggestions for how I can debug
this sort of thing without asking Lemma1?  What should I do when I get an
error message that just seems wrong?

Steve

Stephen Brackin
Senior Security Analyst
CygnaCom Solutions, Inc.
an Entrust company
Phone: 607-277-8211 Fax:  607-277-8211
http://www.cygnacom.com

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040916/88bb7bfa/attachment.htm>