Received: by 10.66.79.36 with SMTP id g4mr6042225pax.38.1350549742473;
        Thu, 18 Oct 2012 01:42:22 -0700 (PDT)
Path: s9ni20968pbb.0!nntp.google.com!news.glorb.com!uio.no!nntp.uio.no!.POSTED!not-for-mail
From: Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de>
Newsgroups: fa.isabelle
Subject: Re: [isabelle] Status of "eval" method
Date: Thu, 18 Oct 2012 08:42:22 UTC
Organization: TU Munich
Lines: 47
Sender: cl-isabelle-users-boun...@lists.cam.ac.uk
Message-ID: <fa.Kn82ydcTbHEmsu1205ltcmMarPc@ifi.uio.no>
References: <fa.e9lU5HAuzHi4jlsVZ+2UngOdL3Q@ifi.uio.no>
NNTP-Posting-Host: mail-jess.uio.no
Mime-Version: 1.0
Content-Type: multipart/signed; micalg=pgp-sha1;
	protocol="application/pgp-signature";
	boundary="------------enig46D0B2C3EDF99443AC65CF5A"
X-Trace: readme.uio.no 1350549742 10383 129.240.7.9 (18 Oct 2012 08:42:22 GMT)
X-Complaints-To: abuse@uio.no
NNTP-Posting-Date: Thu, 18 Oct 2012 08:42:22 +0000 (UTC)
User-Agent: Mozilla/5.0 (X11; Linux i686;
	rv:16.0) Gecko/20121011 Thunderbird/16.0.1
To: cl-isabelle-us...@lists.cam.ac.uk
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.7 from SpamAssassin-3.3.2-1399152 
	* -2.3 RCVD_IN_DNSWL_MED RBL: Sender listed at http://www.dnswl.org/,
	*      medium trust
	*      [131.159.0.8 listed in list.dnswl.dnsbl.ja.net]
	* -0.4 RP_MATCHES_RCVD Envelope sender domain matches handover relay
	*      domain
X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/
X-Virus-Scanned: amavisd-new at informatik.tu-muenchen.de
In-Reply-To: <1350459384.4952.69.camel@lapbroy33>
X-Enigmail-Version: 1.4.5
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: Thu, 18 Oct 2012 10:36:21 +0200
Original-Message-Id: <507FBF85.30...@informatik.tu-muenchen.de>
Original-References: <1350459384.4952.69.camel@lapbroy33>

This is an OpenPGP/MIME signed message (RFC 2440 and 3156)
--------------enig46D0B2C3EDF99443AC65CF5A
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

> a student of mine recently noticed that there is no documentation for
> the "eval" method. Nevertheless, he was able to find it. What he of
> course did not recognize was, that it actually seems to "prove" theorems
> by cheating (they are pretty-printed with [!] afterwards). 
> 
> So I propose to either add proper documentation for this method,
> including a warning that it does not go through the inference kernel,
> perhaps even renaming it to something like "eval_sorry", or to remove
> it.

»eval« is the successor of the »evaluation« method, which wasn't ever
documented thoroughly either (at least I guess so, otherwise I would
have migrated that documentation).

If all methods relying on oracles are supposed to reflect this in their
name, there are a couple of other candidates also, e.g. normalizsation.
 Keep this in mind when discussing renames etc.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


--------------enig46D0B2C3EDF99443AC65CF5A
Content-Type: application/pgp-signature; name="signature.asc"
Content-Description: OpenPGP digital signature
Content-Disposition: attachment; filename="signature.asc"

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://www.enigmail.net/

iEYEARECAAYFAlB/v4oACgkQZEASYmKQGuHflQCgk63TSwvhFtLK6q6yWs2K4of1
GuUAoK1BeFUuwgTEfwiV9g054xmECuZ1
=a5Cr
-----END PGP SIGNATURE-----

--------------enig46D0B2C3EDF99443AC65CF5A--