Handle more exception cases directly in proof code. Update thesis!
Small fixes.