Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command
I was replacing some 'def "f == %x. P x"' by the new 'define' command
and have two comments:
1) For 'definition' the constant name and the 'where' can be dropped, e.g.,
definition "f = ..."
I do this a lot, because
definition f where "f = ..."
seems a bit silly (I mostly do this whenever I deem the type of "f" to
be so obvious that I do not want to state it explicitly). I would like
to have the same option also for 'define'.
2) I would have guessed (but reading isar-ref showed me otherwise) that
define f where "f x = P x"
is (almost) the same as
define f where "f = (%x. P x)"
but for that I need
define f where "f x = P x" for x
While this is consistent with 'have ... if ... for ...' it is different
from what 'definition' does, and for some reason I was expecting to
behave 'define' very similar to 'definition' (it might have been the
name ;)). Is there a specific reason that arguments of the left-hand
side of 'define' are not meta-all-quantified implicitly?
On 11/22/2016 10:36 AM, Makarius wrote:
> Dear Isabelle users,
> after more than 2 weeks, here is the next release candidate for
> Isabelle2016-1 (December 2016):
> http://isabelle.in.tum.de/website-Isabelle2016-1-RC3 -- see also
> More fine points have been consolidated. A component for the new
> experimental Nunchaku tool has been included.
> The corresponding repository versions of Isabelle and AFP are
> and https://bitbucket.org/isa-afp/afp-devel/commits/1a3901597f0f
> It is also possible to follow nightly development snapshots from
> http://isabelle.in.tum.de/devel although they might be somewhat erratic.
> At this stage, Isabelle release candidates are already sufficiently
> consolidated to be ready for everyday use. Adapting your applications
> now gives a unique chance for feedback before the release is finalized.
> When discussing problems, observations, suggestions, etc. the mail
> subject line should be changed to something informative, and the
> particular Isabelle version given in the message body.
This archive was generated by a fusion of
Pipermail (Mailman edition) and