[isabelle] 0::'a



In ProofGeneral, numerals of type 'a are explicitly flagged with their type in
the output. It is an incredibly useful little feature, not just but in
particular for novices. Which is why we introduced it. Any reason not to have it
with jedit as well?

Tobias




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