src/HOL/ROOT
changeset 51236 f301ad90c48b
parent 51161 6ed12ae3b3e1
child 51263 31e786e0e6a7
--- a/src/HOL/ROOT	Thu Feb 21 16:00:48 2013 +0100
+++ b/src/HOL/ROOT	Thu Feb 21 18:21:40 2013 +0100
@@ -224,7 +224,7 @@
     "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
@@ -232,7 +232,6 @@
     Verifying security protocols using UNITY.
   *}
   options [document_graph]
-  theories [document = false] "../Auth/Public"
   theories
     (*Basic meta-theory*)
     "UNITY_Main"
@@ -276,12 +275,10 @@
   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"