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
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
