diff -r 105715a0a807 -r 598409a21f4c ROOT --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ROOT Thu Jun 20 13:50:01 2013 -0400 @@ -0,0 +1,22 @@ +session "PIP" = HOL + + theories [document = false] + "CpsG" + "ExtGG" + +session "Slides2" in "Slides" = PIP + + options [document = pdf, browser_info = false, document_output = "..", document_variants="slides2"] + theories [document = false] + "~~/src/HOL/Library/LaTeXsugar" + theories[document = true] + "Slides2" + files + "document/build" + +session "Slides3" in "Slides" = PIP + + options [document = pdf, browser_info = false, document_output = "..", document_variants="slides3"] + theories [document = false] + "~~/src/HOL/Library/LaTeXsugar" + theories[document = true, show_question_marks = false] + "Slides3" + files + "document/build" \ No newline at end of file