more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
--- 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"