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