> I agree that a separate theory would be nice. But before doing so, we
> should also try to consolidate what's there already. The current state
> in List.thy is as follows (8c0a27b9c1bd):
>
> 1. lexord :: ('a * 'a) set => ('a list * 'a list) set
>a set version of the irreflexive lexicographic
Which version of Isabelle are you using, and which one have you used
before, that was stable?
--
Peter
On Mo, 2013-12-02 at 23:29 +, Peter Maximilian Hirschbeck wrote:
> Die aktuelle Hausaufgabe ist im Anhang, oder zumindest das was davon übrig
> geblieben ist. Leider hat Isabelle bei ei
