more formal theory and session names;
tuned whitespace;