--- a/ROOT Tue Dec 15 21:45:46 2015 +0800 +++ b/ROOT Tue Dec 15 15:10:40 2015 +0000 @@ -1,5 +1,5 @@ session "PIP" = HOL + - theories [document = false] + theories [document = false, quick_and_dirty] "CpsG" "ExtGG" "Test"