Email Gateway (Aug 19 2022 at 12:06): Email Gateway (Aug 19 2022 at 12:06):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
some (mostly unimportant) comments and questions on the extended
documentation of the function package (nice to have the new elim/cases
rules!):
"A definition of function f" -> "The definition of a function f"
(Otherwise it sounds like only "f", and no other function, gives rise to
the new rules.)
"also tell us" -> "also tells us" (Since "the rule", independent of
its name, is singular.)
"elim rules above" -> "elims rule above" (?) (Why is "elim" typeset as
it is? Should this refer to the name of the fact, or the "elim" attribute?)
In the example lemma, how about the more "canonical"
lemma
assumes "list_to_option xs = y"
shows "P"
using assms
proof (rule list_to_option.elims)
fix x
assume "xs = [x]" and "y = Some x"
then show "P" sorry
next
assume "xs = []" and "y = None"
then show "P" sorry
next
fix a b xs'
assume "xs = a # b # xs'" and "y = None"
then show "P" sorry
qed
instead of using the old-school "erule"?
In general, why is the name "f.elims" (rather than "f.elim")? Won't
this be a single rule in most cases? Only for mutually recursive
functions there are more? Or do I miss something? (Sorry if this was
discussed before.)
Btw: A few words on what happens for mutually recursive functions
might be helpful (e.g., with the "standard" definition of "even"/"odd" I
end up with 3 rules in each of "even.elims" and "odd.elims").
cheers
chris
Email Gateway (Aug 19 2022 at 12:22):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
another release candidate is available here:
http://isabelle.in.tum.de/website-Isabelle2013-1-RC2
Notable changes wrt. Isabelle2013-1-RC1:
* Explicit binary executable even for Linux -- modern desktops no longer
consider an executable script as executable to be clicked on.
* Mac OS X Snow Leopard is de-facto discontinued. Normally we support
the 3 latest Mac OS X versions, and Mavericks is not available yet,
but current versions of Java 7 and jEdit appear to have fundamental
problems with this old operating system that Oracle never intended to
support in the first place.
* Various re-adjustments in the dynamics of Sledgehammer, both the
implicit "auto" mode and the explicit GUI panel.
See also https://bitbucket.org/isabelle_project/isabelle-release for the
main website where the final stage before Isabelle2013-1 is organized.
There is also a link to an issue tracker on the same Bitbucket site.
Observations from testing release candidates may be discussed here on
isabelle-users (not isabelle-dev), on the bitbucket tracker, or via
private mail.
Makarius
Email Gateway (Aug 19 2022 at 12:22):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-09 13:55 Makarius:
* Explicit binary executable even for Linux -- modern desktops no longer
consider an executable script as executable to be clicked on.
Wouldn't it be easier to provide a *.desktop file instead? (See
https://wiki.archlinux.org/index.php/Desktop_Entries for documentation.)
I think these are widely understood across Linux desktop environments.
Just a suggestion; I start Isabelle from the command line anyway.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:23):From: Makarius <makarius@sketis.net>
I was trying that recently, but the freedesktop.org standardization
committee does not support the idea of relative paths in .desktop
specifications. See also
http://lists.freedesktop.org/archives/xdg/2011-June/011992.html
Thus an application has to be globally installed on the system. It is
just the old problem of many Linux communities of treating system software
and application software as one and the same, with many problems coming
from it.
Are you actually using Arch Linux yourself, or is the above URL just an
accident? I am just trying to tick major Linux fractions as "tested",
although for Arch everybody needs to start from scratch anyway in the
selection of packages so it is hard to test anything once and for all.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC