Re: [isabelle-dev] Problem with let-simproc

2013-02-06 Thread Thomas Sewell
I'd forgotten I'd ever reported this to you. My problems with let_simproc run a little deeper anyway, and I've moved to a different approach in the meanwhile. Sorry if I've left you labouring on my behalf. Yours, Thomas. On 07/02/13 02:38, Johannes Hölzl wrote: Am Mittwoch, den 06.02.20

Re: [isabelle-dev] Problem with let-simproc

2013-02-06 Thread Johannes Hölzl
Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius: > On Tue, 5 Feb 2013, Johannes Hölzl wrote: > > > there is a bugproblem with the let-simproc, resulting in a non > > terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of > > isabelle-release): > > > > theory Scratch imports Comple

Re: [isabelle-dev] isabelle.in.tum.de web server encoding

2013-02-06 Thread Christian Sternagel
Just as a further data point: when visiting http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS using firefox (on Linux) where the default encoding on the client side is "Western ISO-8859-1" then some symbols are strange. If I explicitly set the encoding to

Re: [isabelle-dev] isabelle.in.tum.de web server encoding

2013-02-06 Thread Gergely Buday
Well, google helps: http://stackoverflow.com/questions/913869/how-to-change-the-default-encoding-to-utf-8-for-server - Gergely On 6 February 2013 13:20, Makarius wrote: > Dear Apache experts, > > some days ago I noticed the famous French problem > http://www.apprendre-en-ligne.net/bloginfo/inde

[isabelle-dev] isabelle.in.tum.de web server encoding

2013-02-06 Thread Makarius
Dear Apache experts, some days ago I noticed the famous French problem http://www.apprendre-en-ligne.net/bloginfo/index.php/2009/01/21/151-martine-ecrit-en-utf-8 on the TUM web server. This affects names in http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS

Re: [isabelle-dev] Problem with let-simproc

2013-02-06 Thread Makarius
On Tue, 5 Feb 2013, Johannes Hölzl wrote: there is a bugproblem with the let-simproc, resulting in a non terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of isabelle-release): theory Scratch imports Complex_Main begin lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X" using [[