Roger,
When I execute:
a (REPEAT z_strip_tac
THEN POP_ASM_T ante_tac
THEN asm_rewrite_tac[]);
ProofPower returns the following message:
:# :# Exception- Fail * the assumption list is empty [POP_ASM_T.9302] *
raised
Exception+ Fail * the assumption list is empty [POP_ASM_T.9302] * raised
Is everything fine?
Artur
2009/3/24 Roger Bishop Jones <r...@rbjones.com>
> Artur,
>
> On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote:
>
> >The problem is: only for those cases,
> >what I choose as witness does not satisfy the predicate.
>
> Well, any sequence of length 1 (or zero?) does for the
> first case. Proof attached.
>
> If you still can't crack the other two send me your
> best attempt.
>
> Roger
>
>
> _______________________________________________
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>
>
--
Artur Oliveira Gomes
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
