Hi all, Reminder: I will be holding the following talk at 14:00: Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. If you've seen it already, you probably want to show up at 15:30 for Michael's talk on his project, which is about ontology evolution. Jasmin