On Thu, 10 Jan 2013, Steffen Juilf Smolka wrote:
Is this the intended behaviour? It used to be different a couple of
month ago. I don't know when it changed exacyly, but I think changeset
a6814de45b69 might be responsible for the change.
Yes, that change is in the vicinity where I was
There might be corner cases where the change of the display leads to odd
effects. Are there concrete incidents already that need to be reconsidered
before the release?
We use Syntax.string_of_term when creating Isar proof scripts in Sledgehammer
and rely on Type.contstraint to introduce
On Fri, 11 Jan 2013, Steffen Juilf Smolka wrote:
We use Syntax.string_of_term when creating Isar proof scripts in
Sledgehammer and rely on Type.contstraint to introduce type annotations
in terms (this does not work with show_markup set to true).
Yes, it is correct to set show_markup=false in
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
Is this the intended behaviour? It used to be different a couple of month ago.
I don't know when it changed
