[isabelle-dev] »real« considered harmful

Manuel Eberl eberlm at in.tum.de
Wed Jun 24 16:01:40 CEST 2015

On 24/06/15 15:55, Larry Paulson wrote:
> A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on.
When I type ‘term "sqrt (of_nat 2)"’ and hover over the ‘of_nat’, it 
says ‘constant "Nat.semiring_1_class.of_nat" :: nat ⇒ real’.

More information about the isabelle-dev mailing list