ROOT
changeset 43 45e1d324c493
parent 39 7ea6b019ce24
child 45 fc83f79009bd
equal deleted inserted replaced
42:0069bca6dd51 43:45e1d324c493
     1 session "PIP" = HOL +
     1 session "PIP" = HOL +
     2   theories [document = false]
     2   theories [document = false]
     3 	"CpsG" 
     3 	"CpsG" 
     4 	"ExtGG"
     4 	"ExtGG"
     5         "Test" 
     5         (* "Test" *)
     6 
     6 
     7 session "Slides2" in "Slides" = PIP +
     7 session "Slides2" in "Slides" = PIP +
     8   options [document_variants="slides2"]
     8   options [document_variants="slides2"]
     9   theories [document = false]
     9   theories [document = false]
    10     "~~/src/HOL/Library/LaTeXsugar"
    10     "~~/src/HOL/Library/LaTeXsugar"