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


Am Donnerstag, den 04.10.2012, 10:57 +0200 schrieb Jasmin Blanchette:
> Could you specify precisely which version of Nominal2 and of Isabelle you're using? I'm using the latest of both and get this error from Nominal2:

I am using 87d1e815aa59 for Nominal2, but it is reproducible with the
tarball from; both on the
Isabelle2012 release.

> That certainly sounds strange. Are the goals really identical, or is
> one using metaequality and the other object-level equality?

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,

Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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