Received: by 10.181.13.75 with SMTP id ew11mr1560320wid.0.1351484305368;
        Sun, 28 Oct 2012 21:18:25 -0700 (PDT)
Path: q13ni92678wii.0!nntp.google.com!feeder3.cambriumusenet.nl!feed.tweaknews.nl!216.196.110.142.MISMATCH!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!news.nobody.at!goblin1!goblin.stu.neva.ru!uio.no!nntp.uio.no!.POSTED!not-for-mail
From: Mathieu Giorgino <Mathieu.Giorg...@irit.fr>
Newsgroups: fa.isabelle
Subject: Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to
 beta-normalization issue
Date: Fri, 26 Oct 2012 13:16:52 UTC
Organization: IRIT
Lines: 37
Sender: cl-isabelle-users-boun...@lists.cam.ac.uk
Message-ID: <fa.amg8aAWbi+070UwXI9pzlzsTXr0@ifi.uio.no>
References: <fa.ekSKzUInHvNvY6Hwtt/dLzb1zL4@ifi.uio.no> <fa.3jC8GvqiqaemLUdjHukxLhpN8/E@ifi.uio.no> <fa.6KptDKZ5N5xM/Dg0hxHB2nEHfd8@ifi.uio.no> <fa.ucCxSIMA6V0Mzor+JfZ93LD3cIM@ifi.uio.no> <fa.uwPyurgbNUlLDg3lHw+zxasvgpg@ifi.uio.no>
NNTP-Posting-Host: mail-jess.uio.no
Mime-Version: 1.0
X-Trace: readme.uio.no 1351257412 4084 129.240.7.9 (26 Oct 2012 13:16:52 GMT)
X-Complaints-To: abuse@uio.no
NNTP-Posting-Date: Fri, 26 Oct 2012 13:16:52 +0000 (UTC)
User-Agent: Mozilla/5.0 (X11; Linux x86_64;
	rv:15.0) Gecko/20120910 Thunderbird/15.0.1
Cc: Christian Sternagel <c-ste...@jaist.ac.jp>,
	cl-isabelle-us...@lists.cam.ac.uk
To: Andreas Lochbihler <andreas.lochbih...@kit.edu>
X-Cam-AntiVirus: not scanned (internal relaying)
X-Cam-SpamDetails: not scanned
X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/
X-Cam-AntiVirus: no malware found
X-Cam-SpamDetails: score -2.3 from SpamAssassin-3.3.2-1402026 
	* -2.3 RCVD_IN_DNSWL_MED RBL: Sender listed at http://www.dnswl.org/,
	*      medium trust
	*      [195.220.59.41 listed in list.dnswl.dnsbl.ja.net]
X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/
In-Reply-To: <508A3993.6030806@kit.edu>
X-Virus-Scanned: clamav-milter 0.97.3 at smtp1.cict.fr
X-Virus-Status: Clean
X-MIME-Autoconverted: from 8bit to quoted-printable by smtp1.cict.fr id
	q9QDBgU0029939
X-BeenThere: cl-isabelle-us...@lists.cam.ac.uk
X-Mailman-Version: 2.1.8
List-Id: Isabelle Users List <cl-isabelle-users.lists.cam.ac.uk>
List-Unsubscribe: <https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users>, 
	<mailto:cl-isabelle-users-requ...@lists.cam.ac.uk?subject=unsubscribe>
List-Archive: <https://lists.cam.ac.uk/pipermail/cl-isabelle-users>
List-Post: <mailto:cl-isabelle-us...@lists.cam.ac.uk>
List-Help: <mailto:cl-isabelle-users-requ...@lists.cam.ac.uk?subject=help>
List-Subscribe: <https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users>, 
	<mailto:cl-isabelle-users-requ...@lists.cam.ac.uk?subject=subscribe>
Original-Date: Fri, 26 Oct 2012 15:09:38 +0200
Original-Message-Id: <508A8B92.4020...@irit.fr>
Original-References: <1350924337.3906.54.camel@lapbroy33>	<alpine.LNX.2.00.1210222057450.14...@macbroy20.informatik.tu-muenchen.de>	<1350977142.3906.79.camel@lapbroy33>	<alpine.LNX.2.00.1210231326060.23...@macbroy20.informatik.tu-muenchen.de>	<32ED3FDA-4B43-4F98-B52C-7752402D6...@cam.ac.uk>	<alpine.LNX.2.00.1210231529430.7...@macbroy20.informatik.tu-muenchen.de>
	<508A34E3.9020...@jaist.ac.jp> <508A3993.6030...@kit.edu>
Bytes: 4361
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 8bit

It seems most of the links on this page are broken. An easy fix is to 
replace all occurences of
   "tphols.in.tum.de"
by
   "isabelle.in.tum.de/nominal/activities/tphols09/"
in the html file.

Thanks for the link.

- Mathieu

Le 26/10/2012 09:19, Andreas Lochbihler a �crit :
> Hi Christian,
>
> the website still has the theory files.
>
> http://isabelle.in.tum.de/nominal/activities/tphols09/idw.html
>
> Andreas
>
> Am 26.10.2012 08:59, schrieb Christian Sternagel:
>>> What I found quite interesting was the presentation by Stefan Berghofer
>>> of Isabelle conversions at the 2009 isabelle-dev workshop at Munich. He
>>> first showed how to make a simplifier with a few conversions and
>>> conversion combinators, then showed how to make it a little faster using
>>> a "Boultonized" version of the same (like "Q" conversions in HOL), and
>>> then showed how to make it really fast using the Isabelle Simplifier
>>> techniques that came after conversions so many years ago.
>> Does anybody know whether slides/thy-files of this talk are still
>> around? (I did
>> not manage to find a website for any of the Isabelle Users Workshops
>> besides
>> 2012.) - cheers chris
>>
>