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 :
It seems that the required changes are minimal. See the attached patch. To be on the s
Dear Makarius,
On 10/01/2013 06:48 AM, Makarius wrote:
On Wed, 11 Sep 2013, Makarius wrote:
Doing some web search while trying, I've found suspicious problem
reports like this:
iBus breaks keyboard input for java apps -- Feb 21, 2012
http://code.google.com/p/ibus/issues/detail?id=1417
It
On Mon, Sep 30, 2013 at 2:34 PM, Makarius 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
> historical reasons f
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 virtu
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".
"F
On Fri, Sep 27, 2013 at 12:16 PM, Florian Haftmann
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 problem with the context here.
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 so
On 9/30/2013 6:10 AM, Makarius wrote:
There could be some nice videos instead, but I still don't know how to
produce them.
The most popular screen-capture software for instructional videos is
Camtasia:
1) http://www.techsmith.com/camtasia.html
2) Docs: http://www.techsmith.com/tutorial-camta
Am 30.09.2013 um 15:07 schrieb Christian Sternagel :
> 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 AFP that
> containe
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
AFP that contained the keyword "adhoc_overloading" in Isabelle/jEdit
instead o
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 ch
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 "http://isabelle.in.tum.de/components
> 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
k
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
happen
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 upda
Early in 2013 I was planning to update the old PG-based movie to use jEdit, but
was interrupted by massive programme committee obligations among other things,
and it was left behind by events. And anyway jEdit has changed quite a bit
since then. Perhaps I shall find the time after the next relea
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 "http://isabelle.in.tum.de/components/jdk-7u40.tar.gz";
Unpacking "/home/lars/.isabe
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 app
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 / Install
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 publ
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
https://bitbucket.org/
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
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 changeset here, or send it to me pr
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 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
25 matches
Mail list logo
