[isabelle] Variables in locale assumptions



Dear all,

In Isabelle/jEdit 2013-2, the following locale works fine:

locale Test =
  fixes pred :: "'a set ⇒ 'a rel ⇒ bool"
  assumes a1: "pred S R"
(*  assumes a2: "pred R S" *)
begin
lemma pred_is_UNIV: "pred A B"
  by (metis a1)
end

However, uncommenting assumption a2 gives me the following error:

Type unification failed
Type error in application: incompatible operand type
Operator:  pred :: 'a set ⇒ ('a × 'a) set ⇒ bool
Operand:   R :: ('a × 'a) set

Page 2 of the locale tutorial seems to suggest that this is a bug. Or should I expect this behaviour?

Thanks in advance!
Stephan




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