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



Hi,

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 http://isabelle.in.tum.de/nominal/download; 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,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

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



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