[isabelle] Variables in locale assumptions
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" *)
lemma pred_is_UNIV: "pred A B"
by (metis a1)
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and