Re: [isabelle] Isabelle2016-1-RC3 available for testing: new define command

Dear Makarius,

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):
> -- 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
> It is also possible to follow nightly development snapshots from
> 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.
> 	Makarius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.