First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms. Please find the results
of my
The Lehrstuhl at TUM has this ancient tradition to hand out full root
access (via the isabelle Unix group) to anybody who happens to get an
account for any kind of project.
This is a lot of power (and responsibility) and and recent years we had
quite often the situation that neither the one
On Tue, 9 Jul 2013, Tjark Weber wrote:
On Mon, 2013-07-08 at 11:09 +0200, Makarius wrote:
Does the Isabelle tool dimacs2hol from 2004 still have a purpose?
The DIMACS CNF format appears to be an old proposal for SAT, predating
newer things like SMT-LIB. So this looks like a candidate for
Markus Westerlind is a student of mine.
For his Bachelor's thesis he needs to carry out performance measurements on a
machine with many cores (isabelle-server).
His project is not directly related to Isabelle, so you are right that a full
root access is too much, but it is the only way for him
On Wed, 10 Jul 2013, Fabian Immler wrote:
Markus Westerlind is a student of mine. For his Bachelor's thesis he
needs to carry out performance measurements on a machine with many cores
(isabelle-server). His project is not directly related to Isabelle, so
you are right that a full root access
Exactly the same applies to Yutaka.
Fabian
Am 10.07.2013 um 13:30 schrieb Makarius makar...@sketis.net:
On Wed, 10 Jul 2013, Fabian Immler wrote:
Markus Westerlind is a student of mine. For his Bachelor's thesis he needs
to carry out performance measurements on a machine with many cores
On Wed, 10 Jul 2013, Fabian Immler wrote:
For his Bachelor's thesis he needs to carry out performance measurements
on a machine with many cores (isabelle-server).
What is this project anyway?
Note that isabelle-server has many cores (24), but the hardware structure
is made for many
Am 10.07.2013 um 13:54 schrieb Makarius makar...@sketis.net:
On Wed, 10 Jul 2013, Fabian Immler wrote:
For his Bachelor's thesis he needs to carry out performance measurements on
a machine with many cores (isabelle-server).
What is this project anyway?
It is about evaluating libraries
This is just a reminder of an important point that I am trying to make for
many months already:
PolyML.makestring has no practical purpose outside bootstrapping of
Isabelle/Pure. Most people can forget that it ever existed.
The @{make_string} antiquotation does a better job, with proper
This is an update of this important thread.
It turned out that the symmetric version where both \^sub and \^sup
are allowed in the liberal part of identifiers works, with minimal impact
on applications of the known universe.
So the reformed identifier syntax is like this:
LETTER = A .. Z
On Wed, 3 Jul 2013, Florian Haftmann wrote:
It sounds like I should also look into the AFP. Is
http://hg.code.sf.net/p/afp/code the correct repo URL?
Yse, indeed.
This is where I've got via the sourceforge project summary:
http://sourceforge.net/projects/afp/
Mercurial / Code then points
On 10.07.2013 17:29, Makarius wrote:
Is there a proper way to access AFP history on the web
What about the clone at TUM, i.e. http://isabelle.in.tum.de/repos/AFP/?
This should be updated regularly by Mira.
-- Lars
___
isabelle-dev mailing list
Am 10/07/2013 16:54, schrieb Makarius:
That is an instance of \^supLETTER, i.e. the remaining overlap from the
earlier discussion on this thread. I have presently escaped the situation by
using \^bsup \^esup which looks almost the same in Latex, but is a bit
awkward in Isabelle/jEdit.
Why
On Wed, 10 Jul 2013, Tobias Nipkow wrote:
Am 10/07/2013 16:54, schrieb Makarius:
That is an instance of \^supLETTER, i.e. the remaining overlap from the
earlier discussion on this thread. I have presently escaped the situation by
using \^bsup \^esup which looks almost the same in Latex, but
On Wed, 10 Jul 2013, Lars Noschinski wrote:
On 10.07.2013 17:29, Makarius wrote:
Is there a proper way to access AFP history on the web
What about the clone at TUM, i.e. http://isabelle.in.tum.de/repos/AFP/?
This should be updated regularly by Mira.
Looks fine to me.
What do the AFP
I don't think that's a good idea.
The official URL for browsing is
http://sourceforge.net/p/afp/code/ci/default/tree/ as advertised on
http://afp.sourceforge.net/download.shtml.
The official URL for cloning is http://hg.code.sf.net/p/afp/code as advertised
on that page (with ssh and SF login
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match for that
matter)?
My question arises as follows. In adhoc_overloading.ML previously
Sign.the_const_type was used to obtain the type of a constant.
Hi Chris,
I think Variable.polymorphic is what you want to use before using
fastype_of.
Dmitriy
Am 11.07.2013 05:12, schrieb Christian Sternagel:
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match
18 matches
Mail list logo
