@INPROCEEDINGS{merz:weak-alternating, title = "Weak Alternating Automata in {I}sabelle/{HOL}", author = "Stephan Merz", editor = "J. Harrison and M. Aagaard", booktitle = "Theorem Proving in Higher Order Logics: 13th Intl. Conf., TPHOLs 2000", series = "Lecture Notes in Computer Science", volume = 1869, year = 2000, publisher = "Springer-Verlag", pages = "423--440" }