# HG changeset patch
# User wenzelm
# Date 1361467300 -3600
# Node ID f301ad90c48b87670429d180a2b42bae1566a86d
# Parent  8333c10d1a6d278f7c9330f6b5a912da523ab27b
more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;

diff -r 8333c10d1a6d -r f301ad90c48b src/HOL/ROOT
--- 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"