o commented out trace statements
o changed the testing tools to not compile on their own.
Added the possibility of referring to theorems (in addition to axioms) in proofs