[isabelle-dev] Pow

Alexander Krauss krauss at in.tum.de
Mon Dec 14 16:34:43 CET 2009


Robert Himmelmann wrote:
> There seem to be quite a few problems with find_theorems at the moment;
> various searches do not return any results, e.g. prepending (100) to any
> search. Changeset a03f3f9874f6 seems to be working whereas in
> ada58d813783 the search is broken.

The culprit seems to be f3f0e20923a7, which changed the semantics of 
take and drop with negative indices. Errors in find theorems are not 
caught by the usual regression tests, unfortunately...

changeset:   34059:f3f0e20923a7
user:        haftmann
date:        Wed Dec 09 21:38:12 2009 +0100
summary:     take and drop as projections of chop


Alex



More information about the isabelle-dev mailing list