[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