added ability to initialize mutexes, and a roadmap for supporting recursive and errorchecking locks
refined parentheses on theorem macros