On 14/09/12 18:48, Roger Bishop Jones wrote:
(I attach a revised version of your document with the proof
fixed).

In order for z_get_spec to drop the consistency hypothesis, it is necessary to use save_consistency_thm on the resulting theorem. So after the proof you need a line like:

save_consistency_thm %SZT%masterStop%>% (pop_thm ());

I tend to write such proofs with the following form, for some global variable C:

save_consistency_thm %SZT%C%>% (
z_push_consistency_thm %SZT%C%>%;

(* proof steps here *)

pop_thm ()
);

Phil


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

Reply via email to