1 session "PIP" = HOL +

     1 session "PIP" = HOL +

     2   theories [document = false, quick_and_dirty]

     2   theories [document = false, quick_and_dirty]

     3 	"Implementation" 

     3 	"Implementation" 

     4 	"Correctness"

     4 	"Correctness"

     6 

     5 

     7 session "Slides2" in "Slides" = PIP +

     6 session "Slides2" in "Slides" = PIP +

     8   options [document_variants="slides2"]

     7   options [document_variants="slides2"]

     9   theories [document = false]

     8   theories [document = false]

    10     "~~/src/HOL/Library/LaTeXsugar"

     9     "~~/src/HOL/Library/LaTeXsugar"