Hi Chris,
[...]
When defining a function f, whose result type is T, it might be
necessary to peek under the hood in order to show termination. When
doing this manually, we destroy the abstraction and always have to
reason about the raw-level and even worse, also all the existing
constants with
On 08/17/2013 04:05 PM, Makarius wrote:
in the past few weeks the coming release has been mentioned in passing
several times. So far the precise schedule is not clear, but just from
the distance to Isabelle2013 and the amount of material that is about to
be finished for Isabelle2013-1, it has
