[isabelle-dev] JEdit: type constraints no longer printed by default

Lars Noschinski noschinl at in.tum.de
Thu Jan 10 17:37:32 CET 2013


On 10.01.2013 17:24, Steffen Juilf Smolka wrote:
> In af8ecf09a58c, type constraints are no longer printed by default in JEdit:
>
> ML {*
> @{term "f"}
> |> Type.constraint @{typ "nat => nat"}
> |> Syntax.string_of_term @{context}
> |> writeln
> *}
>
> # f

With show_markup set, you see the type contstraints the same way as in 
the input text, by hovering with Ctrl pressed.

   -- Lars



More information about the isabelle-dev mailing list