On Thu, 19 Sep 2013, Makarius wrote:
On Tue, 17 Sep 2013, Jasmin Blanchette wrote:
I had the same issue with Monaco, which is definitely a standard Mac font.
I have played with this font a bit, but did not see anything suspicious so
far. I will use it more often in my office.
Since the
On Mon, 23 Sep 2013, Manuel Eberl wrote:
I sent my changes to Alexander Krauss last Wednesday so that he can
review them.
We are now getting very close to the fork-point for the release. So can
you just post the changeset here, or send it to me privately?
Makarius
On Tue, 24 Sep 2013, Christian Sternagel wrote:
After this changeset, variants may be arbitrary terms (due to
localization). Now replacing a variant by the corresponding overloaded
constant is done by rewriting (as Florian already pointed out, this
happens in insert_overloaded) as follows
Dear all,
this is the last call for small amendments and finalization on the main
Isabelle repository.
Unless there are any last-minute surprises, the fork for Isabelle2013-1
will happen Thu 03-Oct-2013.
This means the history of the official release will continue on
In preparation of Isabelle2013-1 the Isabelle website needs the usual
updating and polishing.
The relevant repository is here:
https://bitbucket.org/isabelle_project/isabelle-website/
Traditionally my main job is to get the Download / Installation part into
shape. I will do that before
Am 30/09/2013 12:45, schrieb Makarius:
In preparation of Isabelle2013-1 the Isabelle website needs the usual updating
and polishing.
The relevant repository is here:
https://bitbucket.org/isabelle_project/isabelle-website/
Traditionally my main job is to get the Download / Installation
On Mon, 30 Sep 2013, Makarius wrote:
Moreover, we should reconsider the old question what to do with
http://isabelle.in.tum.de/overview.html
Further notes on this: the general question is how to ease the first
encounter with Isbaelle after download.
People who have tested the integrated
Maybe this thread is of interest
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03773.html
(It contains an overview.html that I once started but never finished.)
cheers
chris
On 09/30/2013 08:28 PM, Lawrence Paulson wrote:
Early in 2013 I was planning to
On 09/30/2013 07:33 PM, Makarius wrote:
On Tue, 24 Sep 2013, Christian Sternagel wrote:
After this changeset, variants may be arbitrary terms (due to
localization). Now replacing a variant by the corresponding overloaded
constant is done by rewriting (as Florian already pointed out, this
I also tried to download jdk7u40 today (twice), and ran into the very same
problem.
Maybe someone should check the configuration of the web server?
I just mailed the local sysadmins about that issue. Since this seems to
occur every now and then, we'll have to investigate that further. I'll
On Mon, 30 Sep 2013, Stefan Berghofer wrote:
On 09/17/2013 12:28 PM, Lars Hupel wrote:
I was trying to update to the repository version today, but:
$ bin/isabelle components -a
### Missing Isabelle component: /home/lars/.isabelle/contrib/jdk-7u40
Getting
On Mon, 30 Sep 2013, Manuel Eberl wrote:
On 30/09/13 11:49, Makarius wrote:
On Mon, 23 Sep 2013, Manuel Eberl wrote:
I sent my changes to Alexander Krauss last Wednesday so that he can
review them.
We are now getting very close to the fork-point for the release. So
can you just post the
Am 30.09.2013 um 15:07 schrieb Christian Sternagel c.sterna...@gmail.com:
It seems that the required changes are minimal. See the attached patch. To be
on the safe side: could somebody push this to the test server (in my local
tests I just loaded all theories from the Isabelle repo and the
On 9/30/2013 9:12 AM, Gottfried Barrow wrote:
...The audio has too much room reverb in it because his microphone is
not close enough, but it's an example of a site that is constantly
putting out new videos, with the main emphasis on instruction, rather
than flashy video effects...
It's the
On Fri, Sep 27, 2013 at 12:16 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
context field_char_0
begin
…
lemma of_rat_minus: of_rat (- a) = - of_rat a
apply transfer
the »- _« (name uminus) gets replaced by a bound variable »uminusa«.
There seems to be a
On Mon, 30 Sep 2013, Brian Huffman wrote:
1. Always avoid generalizing free variables that are locale
parameters. The problem is that I don't know how to query the context
to find out what they are. (Suggestions, anyone?)
Locale parameters are just one example of regular fixed variables.
On Wed, 11 Sep 2013, Makarius wrote:
On Fri, 6 Sep 2013, Christian Sternagel wrote:
My exact Fedora version is Fedora 19 64-bit with GNOME 3.8.2.
I have made a few attempts to install that somewhat rough Linux distribution,
either virtually or physically, but did not get very far. One
On Mon, Sep 30, 2013 at 2:34 PM, Makarius makar...@sketis.net wrote:
According to the normal context discipline, free variables are always fixed,
like a local const. We have a few tools that violate that principle and
consequently cause confusion, e.g. the Simplifier. There are sometimes
Thanks Jasmin!
@Peter: Does this patch work with your developments as expected?
cheers
chris
On 09/30/2013 10:18 PM, Jasmin Christian Blanchette wrote:
Am 30.09.2013 um 15:07 schrieb Christian Sternagel c.sterna...@gmail.com:
It seems that the required changes are minimal. See the attached
19 matches
Mail list logo
