src/HOL/ROOT

     "Smartcard/Auth_Smartcard"
     "Guard/Auth_Guard_Shared"
     "Guard/Auth_Guard_Public"
   files "document/root.tex"
 
-session "HOL-UNITY" in UNITY = HOL +
+session "HOL-UNITY" in UNITY = "HOL-Auth" +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
     Verifying security protocols using UNITY.
   *}
   options [document_graph]
-  theories [document = false] "../Auth/Public"
   theories
     (*Basic meta-theory*)
     "UNITY_Main"
 
     (*Simple examples: no composition*)

   options [print_mode = "no_brackets,no_type_brackets"]
   theories Unix
   files "document/root.bib" "document/root.tex"
 
 session "HOL-ZF" in ZF = HOL +
-  description {* *}
   theories MainZF Games
   files "document/root.tex"
 
 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
-  description {* *}
   options [document_graph, print_mode = "iff,no_brackets"]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
     "~~/src/HOL/Library/Monad_Syntax"
     "~~/src/HOL/Library/LaTeXsugar"