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 to
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