[isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit



Hi,

when giving the semantics tutorial this morning, I ran into quite
strange tooltips in Isabelle/jedit: Consider, 

theory Scratch
imports Complex_Main
begin

term "∃a::nat. ∃b::real. a+b=0"


when hovering over the a in "a+b" and pressing Ctrl, I get the following
tooltip:
  bound "a"
  bound variable
  :: real

This tooltip is simply wrong! The variable a still has type nat. So I
would have expected either a::nat, or "real a :: real".

--
  Peter









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