Yes, I've seen some of Carsten's demos and they were most impressive. And the automated tactics in Coq and Isabelle also often seem to be able to work some serious magic. But I still have the impression of a certain amount of black art in these things, so I don't want to get too optimistic. :-) - Benjamin