A student has forwarded this problem to me. It seems weird and unbelievable. What have I overlooked?
I tidied it up slightly (see below) but I get the same error message. lemma "True" proof - have "True = (∃x. (λy. True) x)" by simp also have "... = (∃x. (λy. True) x)" oops Larry Begin forwarded message: > From: "W. Li" <[email protected]> > Subject: A possible bug with Isabelle 2013 > Date: 26 February 2013 15:56:58 GMT > To: "L. Paulson" <[email protected]> > > lemma "True" > proof - > have "True=(∃x. (λ_.True) x)" by simp > also have "...=(∃x. (λ_.True) x)" > oops > > Here is the error message: > > Type unification failed: Clash of types "bool" and "_ ⇒ _" > > Type error in application: incompatible operand type > > Operator: op = … :: (??'a itself ⇒ bool) ⇒ bool > Operand: ∃x. True :: bool _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
