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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
