[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