Hi Lukas,
thanks for testing! (Sorry for the late reply, currently my
internet-connectivity is rather sporadic ;)). Please find attached a hg
bundle that does the name change 'rel_comp -> relcomp' for the AFP.
cheers
chris
On 04/04/2012 07:30 PM, Lukas Bulwahn wrote:
Hi Chris,
I have test
On Tue, 3 Apr 2012, Florian Haftmann wrote:
Am 02.04.2012 13:36, schrieb Florian Haftmann:
/mnt/home/isatest/isadist/Isabelle_02-Apr-2012/lib/scripts/run-polyml:
line 77: 27590 Killed "$POLY" -q $ML_OPTIONS
*** Code check failed for SML: "$ISABELLE_PROCESS" -r -q -u Pure
*** At command "expor
On Wed, 4 Apr 2012, Tobias Nipkow wrote:
Am 04/04/2012 11:48, schrieb Tjark Weber:
Adhering to the principle of least astonishment, I suspect an error
message (or at least a warning) would be more helpful.
Isabelle's well-tried principle of least astonishment is not to give too
many helpful
Hi Chris,
I have tested your changeset on the testboard, and a couple of AFP
theories break, cf.
http://isabelle.in.tum.de/testboard/Isabelle/report/edd1df5c8daf4109a6366801aaeff7fd
(Some errors are due to your changes, some are due to current work of
others.)
It might be good to provide some
Am 04/04/2012 11:48, schrieb Tjark Weber:
> Adhering to the principle of least astonishment, I suspect an error
> message (or at least a warning) would be more helpful.
Isabelle's well-tried principle of least astonishment is not to give too many
helpful error messages or warnings ;-)
Actually, i
On Wed, 2012-04-04 at 11:19 +0200, Tobias Nipkow wrote:
> No, a feature. Patterns may not contain repeated variables.
But this is not being enforced; instead, repeated variables are silently
renamed.
Adhering to the principle of least astonishment, I suspect an error
message (or at least a warnin
An updated announcement of a new tutorial in the development version of
Isabelle. Comments welcome! [If it does not build on your own machine, your tex
distribution probably lacks the eulervm package.]
* New tutorial "Programming and Proving in Isabelle/HOL".
It completely supercedes "A Tutorial I
Am 03/04/2012 22:51, schrieb Florian Haftmann:
>>> I'm indedd quite curious, but unable to build the tex sources. The
>>> first error complains about a missing »eulervm.sty«, with lot of
>>> further messages following.
>>
>> You mean you couldn't run the tex sources? Unfortunately I can confirm
>
Hi all,
On 03/31/2012 01:10 AM, Florian Haftmann wrote:
PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with
"relpow").
This would also mean to rename the corresponding lemmas, although I
would also appreciate consistency. Also the »pred_comp« abbreviation
should be droppe
