src/HOL/ROOT
changeset 51236 f301ad90c48b
parent 51161 6ed12ae3b3e1
child 51263 31e786e0e6a7
     1.1 --- a/src/HOL/ROOT	Thu Feb 21 16:00:48 2013 +0100
     1.2 +++ b/src/HOL/ROOT	Thu Feb 21 18:21:40 2013 +0100
     1.3 @@ -224,7 +224,7 @@
     1.4      "Guard/Auth_Guard_Public"
     1.5    files "document/root.tex"
     1.6  
     1.7 -session "HOL-UNITY" in UNITY = HOL +
     1.8 +session "HOL-UNITY" in UNITY = "HOL-Auth" +
     1.9    description {*
    1.10      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.11      Copyright   1998  University of Cambridge
    1.12 @@ -232,7 +232,6 @@
    1.13      Verifying security protocols using UNITY.
    1.14    *}
    1.15    options [document_graph]
    1.16 -  theories [document = false] "../Auth/Public"
    1.17    theories
    1.18      (*Basic meta-theory*)
    1.19      "UNITY_Main"
    1.20 @@ -276,12 +275,10 @@
    1.21    files "document/root.bib" "document/root.tex"
    1.22  
    1.23  session "HOL-ZF" in ZF = HOL +
    1.24 -  description {* *}
    1.25    theories MainZF Games
    1.26    files "document/root.tex"
    1.27  
    1.28  session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
    1.29 -  description {* *}
    1.30    options [document_graph, print_mode = "iff,no_brackets"]
    1.31    theories [document = false]
    1.32      "~~/src/HOL/Library/Countable"