Re: [isabelle] Same proof state, different metis behaviour



Hi Joachim,

Am 04.10.2012 um 11:14 schrieb Joachim Breitner:

> Well, they looked identical... until Andreas told me about 
>  using [[eta_contract=false]]
> and now one (the working) has
> 	⋀p∷perm. p ∙ (λa∷'a fset. fset a) = (λa∷'a fset. fset a)
> and the other has
> 	⋀p∷perm. p ∙ fset = fset
> 
> Sorry for the interruption, please carry on, nothing to see here,

Well, there is something to see here. Ideally, "metis" would behave the same modulo eta. I'll add this to my TODO list (and come back to it after a paper deadline).

Thanks for the report!

Regards,

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.