Just a remark on http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on lexicographic orderings in List.thy is now numerous enough but still self-contained to justify a separate theory Lexorder.thy. I would also suggest that the predicate version should be done using locales rather than the canonical type class.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
