On Mon, 16 Apr 2012, Christian Sternagel wrote:
I drafted a first version of a HOWTO under
https://isabelle.in.tum.de/community/Publish_contributions_as_an_external
Nice summary of the mail thread. As I said, I will not interfere with the
community site directly, but might occasionally
On Mon, 16 Apr 2012, Brian Huffman wrote:
Finally we have a mechanism similar to Section in Coq, a more
lightweight alternative to locales.
This is what Larry Paulson and Florian Kammüller actually started in
1998/1999 and eventually became the fully-featured locale + interpretation
system
On Mon, 16 Apr 2012, Brian Huffman wrote:
Another good use case is recursive functions with many parameters that
don't change in recursive calls. For example, here's a recursion
combinator for binary integers:
context
fixes z0 z1 :: 'a
fixes f0 f1 :: 'a = 'a
begin
function bin_rec :: int
I usually make jokes at a longer historical range.
[...]
Anyway, this thread is diverging. I merely wanted to express my relief
that I can now work in the classic ADT style from the 1970/80-ies almost
unencumbered by ooddities in Isabelle/Scala.
Sorry, I fail to see the joke. If you ask
b) Coding conventions and usual practice (my addition to the above):
It is customary to make constructors, and not some auxiliary
static methods, responsible for proper initialization.
But this is exactly what did not work out smoothly. The task is to make
an implementation of *immutable*
On 04/16/2012 09:13 AM, Christian Sternagel wrote:
Hi all,
On 04/03/2012 02:51 AM, Florian Haftmann wrote:
well, I suggest to augment the existing theory with lemmas transferred
from relpow to relpowp to emphasize that both worlds exists and that
lemmas can be found easier by find_theorems.
On 04/16/2012 11:52 AM, Makarius wrote:
@Lukas: Thanks for pointing me to mercurial queues which are really
a great tool. Using queues it should be easily possible (even as an
external) to avoid the long pilage of private changes and public
commits.
The queues became quite popular early for
Hi all,
I think the possibility to refer to the induction hypothesis via, e.g.,
Suc.IH (for natural numbers) is a nice feature offered by the
induction-wrapper around induct. I was wondering if there is an
inherent problem in the following example, or if the induction-wrapper
could be
