# HG changeset patch
# User wenzelm
# Date 1344440996 -7200
# Node ID f8c1a5b9488f5f968cc89afebdf71cb7b1cf4926
# Parent  f3bbb9ca57d6f46c8d07fa902d5fb9e8ad1ff491
simplified session specifications: names are taken verbatim and current directory is default;

diff -r f3bbb9ca57d6 -r f8c1a5b9488f doc-src/ROOT
--- a/doc-src/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/doc-src/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,10 +1,10 @@
-session Classes! (doc) in "Classes/Thy" = HOL +
+session Classes (doc) in "Classes/Thy" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex"]
   theories [document = false] Setup
   theories Classes
 
-session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
+session Codegen (doc) in "Codegen/Thy" = "HOL-Library" +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
     print_mode = "no_brackets,iff"]
@@ -18,12 +18,12 @@
     Adaptation
     Further
 
-session Functions! (doc) in "Functions/Thy" = HOL +
+session Functions (doc) in "Functions/Thy" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex"]
   theories Functions
 
-session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
+session IsarImplementation (doc) in "IsarImplementation/Thy" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex"]
   theories
@@ -38,7 +38,7 @@
     Syntax
     Tactic
 
-session IsarRef (doc) in "IsarRef/Thy" = HOL +
+session "HOL-IsarRef" (doc) in "IsarRef/Thy" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
     quick_and_dirty]
@@ -59,19 +59,19 @@
     Symbols
     ML_Tactic
 
-session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
+session "HOLCF-IsarRef" (doc) in "IsarRef/Thy" = HOLCF +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
     quick_and_dirty]
   theories HOLCF_Specific
 
-session IsarRef (doc) in "IsarRef/Thy" = ZF +
+session "ZF-IsarRef" (doc) in "IsarRef/Thy" = ZF +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
     quick_and_dirty]
   theories ZF_Specific
 
-session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
+session LaTeXsugar (doc) in "LaTeXsugar/Sugar" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex"]
   theories [document_dump = ""]
@@ -79,7 +79,7 @@
     "~~/src/HOL/Library/OptionalSugar"
   theories Sugar
 
-session Locales! (doc) in "Locales/Locales" = HOL +
+session Locales (doc) in "Locales/Locales" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex"]
   theories
@@ -87,12 +87,12 @@
     Examples2
     Examples3
 
-session Main! (doc) in "Main/Docs" = HOL +
+session Main (doc) in "Main/Docs" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex"]
   theories Main_Doc
 
-session ProgProve! (doc) in "ProgProve/Thys" = HOL +
+session ProgProve (doc) in "ProgProve/Thys" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
     show_question_marks = false]
@@ -104,7 +104,7 @@
     Logic
     Isar
 
-session System! (doc) in "System/Thy" = Pure +
+session System (doc) in "System/Thy" = Pure +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex"]
   theories
@@ -177,11 +177,11 @@
     "Sets/Relations"
     "Sets/Recur"
 
-session ToyList2 (doc) in "TutorialI/ToyList2" = HOL +
+session "HOL-ToyList2" (doc) in "TutorialI/ToyList2" = HOL +
   options [browser_info = false, document = false, print_mode = "brackets"]
   theories ToyList
 
-session examples (doc) in "ZF" = ZF +
+session "ZF-examples" (doc) in "ZF" = ZF +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
     print_mode = "brackets"]
diff -r f3bbb9ca57d6 -r f8c1a5b9488f doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Wed Aug 08 15:58:40 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Wed Aug 08 17:49:56 2012 +0200
@@ -50,7 +50,7 @@
     ;
     body: description? options? ( theories * ) files?
     ;
-    spec: @{syntax name} '!'? groups? dir?
+    spec: @{syntax name} groups? dir?
     ;
     groups: '(' (@{syntax name} +) ')'
     ;
@@ -78,18 +78,9 @@
   applications: only Isabelle/Pure can bootstrap itself from nothing.
 
   All such session specifications together describe a hierarchy (tree)
-  of sessions, with globally unique names.  By default, names are
-  derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"}
-  above.  Cumulatively, this leads to session paths of the form @{text
-  "X\<dash>Y\<dash>Z\<dash>W"}.  Note that in the specification,
-  @{text B} is already such a fully-qualified name, while @{text "A"}
-  is the new base name.
-
-  \item \isakeyword{session}~@{text "A! = B"} indicates a fresh start
-  in the naming scheme: the session is called just @{text "A"} instead
-  of @{text "B\<dash>A"}.  Here the name @{text "A"} should be
-  sufficiently long to stand on its own in a potentially large
-  library.
+  of sessions, with globally unique names.  The new session name
+  @{text "A"} should be sufficiently long to stand on its own in a
+  potentially large library.
 
   \item \isakeyword{session}~@{text "A (groups)"} indicates a
   collection of groups where the new session is a member.  Group names
@@ -100,14 +91,8 @@
   within this unchecked name space.
 
   \item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
-  specifies an explicit directory for this session.  By default,
-  \isakeyword{session}~@{text "A"} abbreviates
-  \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}.  This
-  accommodates the common scheme where some base directory contains
-  several sessions in sub-directories of corresponding names.  Another
-  common scheme is \isakeyword{session}~@{text
-  "A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current
-  directory of the ROOT file.
+  specifies an explicit directory for this session; by default this is
+  the current directory of the @{verbatim ROOT} file.
 
   All theories and auxiliary source files are located relatively to
   the session directory.  The prover process is run within the same as
@@ -143,7 +128,12 @@
 subsubsection {* Examples *}
 
 text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
-  relevant situations. *}
+  relevant situations, but it uses relatively complex quasi-hierarchic
+  naming conventions like @{text "HOL\<dash>SPARK"}, @{text
+  "HOL\<dash>SPARK\<dash>Examples"}.  An alternative is to use
+  unqualified names that are relatively long and descriptive, as in
+  the Archive of Formal Proofs (\url{http://afp.sf.net}), for
+  example. *}
 
 
 section {* System build options \label{sec:system-options} *}
diff -r f3bbb9ca57d6 -r f8c1a5b9488f doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Wed Aug 08 15:58:40 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Wed Aug 08 17:49:56 2012 +0200
@@ -102,10 +102,6 @@
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
 \rail@nont{\isa{groups}}[]
 \rail@endbar
 \rail@bar
@@ -185,17 +181,9 @@
   applications: only Isabelle/Pure can bootstrap itself from nothing.
 
   All such session specifications together describe a hierarchy (tree)
-  of sessions, with globally unique names.  By default, names are
-  derived from parent ones by concatenation, i.e.\ \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}
-  above.  Cumulatively, this leads to session paths of the form \isa{{\isaliteral{22}{\isachardoublequote}}X{\isaliteral{5C3C646173683E}{\isasymdash}}Y{\isaliteral{5C3C646173683E}{\isasymdash}}Z{\isaliteral{5C3C646173683E}{\isasymdash}}W{\isaliteral{22}{\isachardoublequote}}}.  Note that in the specification,
-  \isa{B} is already such a fully-qualified name, while \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}
-  is the new base name.
-
-  \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{21}{\isacharbang}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{22}{\isachardoublequote}}} indicates a fresh start
-  in the naming scheme: the session is called just \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} instead
-  of \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}.  Here the name \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} should be
-  sufficiently long to stand on its own in a potentially large
-  library.
+  of sessions, with globally unique names.  The new session name
+  \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} should be sufficiently long to stand on its own in a
+  potentially large library.
 
   \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{28}{\isacharparenleft}}groups{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} indicates a
   collection of groups where the new session is a member.  Group names
@@ -206,13 +194,8 @@
   within this unchecked name space.
 
   \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}dir{\isaliteral{22}{\isachardoublequote}}}
-  specifies an explicit directory for this session.  By default,
-  \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} abbreviates
-  \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}.  This
-  accommodates the common scheme where some base directory contains
-  several sessions in sub-directories of corresponding names.  Another
-  common scheme is \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\verb|"."| to refer to the current
-  directory of the ROOT file.
+  specifies an explicit directory for this session; by default this is
+  the current directory of the \verb|ROOT| file.
 
   All theories and auxiliary source files are located relatively to
   the session directory.  The prover process is run within the same as
@@ -252,7 +235,11 @@
 %
 \begin{isamarkuptext}%
 See \verb|~~/src/HOL/ROOT| for a diversity of practically
-  relevant situations.%
+  relevant situations, but it uses relatively complex quasi-hierarchic
+  naming conventions like \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{5C3C646173683E}{\isasymdash}}SPARK{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{5C3C646173683E}{\isasymdash}}SPARK{\isaliteral{5C3C646173683E}{\isasymdash}}Examples{\isaliteral{22}{\isachardoublequote}}}.  An alternative is to use
+  unqualified names that are relatively long and descriptive, as in
+  the Archive of Formal Proofs (\url{http://afp.sf.net}), for
+  example.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/CCL/ROOT
--- a/src/CCL/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/CCL/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session CCL! in "." = Pure +
+session CCL = Pure +
   description {*
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -11,7 +11,7 @@
   options [document = false]
   theories Wfd Fix
 
-session ex = CCL +
+session "CCL-ex" in ex = CCL +
   description {*
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/CTT/ROOT
--- a/src/CTT/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/CTT/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session CTT! in "." = Pure +
+session CTT = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -6,7 +6,7 @@
   options [document = false]
   theories Main
 
-session ex = CTT +
+session "CTT-ex" in ex = CTT +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/Cube/ROOT
--- a/src/Cube/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Cube/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session Cube! in "." = Pure +
+session Cube = Pure +
   description {*
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/FOL/ROOT
--- a/src/FOL/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/FOL/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,10 +1,10 @@
-session FOL! in "." = Pure +
+session FOL = Pure +
   description "First-Order Logic with Natural Deduction"
   options [proofs = 2]
   theories FOL
   files "document/root.tex"
 
-session ex = FOL +
+session "FOL-ex" in ex = FOL +
   theories
     First_Order_Logic
     Natural_Numbers
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/FOLP/ROOT
--- a/src/FOLP/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/FOLP/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session FOLP! in "." = Pure +
+session FOLP = Pure +
   description {*
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -10,7 +10,7 @@
   options [document = false]
   theories FOLP
 
-session ex = FOLP +
+session "FOLP-ex" in ex = FOLP +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/HOL/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,30 +1,30 @@
-session HOL! (main) in "." = Pure +
+session HOL (main) = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
   theories Complex_Main
   files "document/root.bib" "document/root.tex"
 
-session "HOL-Base"! in "." = Pure +
+session "HOL-Base" = Pure +
   description {* Raw HOL base, with minimal tools *}
   options [document = false]
   theories HOL
 
-session "HOL-Plain"! in "." = Pure +
+session "HOL-Plain" = Pure +
   description {* HOL side-entry after bootstrap of many tools and packages *}
   options [document = false]
   theories Plain
 
-session "HOL-Main"! in "." = Pure +
+session "HOL-Main" = Pure +
   description {* HOL side-entry for Main only, without Complex_Main *}
   options [document = false]
   theories Main
 
-session "HOL-Proofs"! in "." = Pure +
+session "HOL-Proofs" = Pure +
   description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Main
 
-session Library = HOL +
+session "HOL-Library" in Library = HOL +
   description {* Classical Higher-order Logic -- batteries included *}
   theories
     Library
@@ -41,7 +41,7 @@
     Target_Numeral
   files "document/root.bib" "document/root.tex"
 
-session Hahn_Banach = HOL +
+session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
   description {*
     Author:     Gertrud Bauer, TU Munich
 
@@ -51,7 +51,7 @@
   theories Hahn_Banach
   files "document/root.bib" "document/root.tex"
 
-session Induct = HOL +
+session "HOL-Induct" in Induct = HOL +
   theories [quick_and_dirty]
     Common_Patterns
   theories
@@ -68,7 +68,7 @@
     Com
   files "document/root.tex"
 
-session IMP = HOL +
+session "HOL-IMP" in IMP = HOL +
   options [document_graph]
   theories [document = false]
     "~~/src/HOL/ex/Interpretation_with_Defs"
@@ -109,7 +109,7 @@
     Fold
   files "document/root.bib" "document/root.tex"
 
-session IMPP = HOL +
+session "HOL-IMPP" in IMPP = HOL +
   description {*
     Author:     David von Oheimb
     Copyright   1999 TUM
@@ -117,16 +117,16 @@
   options [document = false]
   theories EvenOdd
 
-session Import = HOL +
+session "HOL-Import" in Import = HOL +
   options [document_graph]
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
-session Number_Theory = HOL +
+session "HOL-Number_Theory" in Number_Theory = HOL +
   options [document = false]
   theories Number_Theory
 
-session Old_Number_Theory = HOL +
+session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
   options [document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Infinite_Set"
@@ -142,20 +142,20 @@
     Pocklington
   files "document/root.tex"
 
-session Hoare = HOL +
+session "HOL-Hoare" in Hoare = HOL +
   theories Hoare
   files "document/root.bib" "document/root.tex"
 
-session Hoare_Parallel = HOL +
+session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
   options [document_graph]
   theories Hoare_Parallel
   files "document/root.bib" "document/root.tex"
 
-session Codegenerator_Test = "HOL-Library" +
+session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   options [document = false, document_graph = false, browser_info = false]
   theories Generate Generate_Pretty RBT_Set_Test
 
-session Metis_Examples = HOL +
+session "HOL-Metis_Examples" in Metis_Examples = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
@@ -174,7 +174,7 @@
     Trans_Closure
     Sets
 
-session Nitpick_Examples = HOL +
+session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
@@ -182,7 +182,7 @@
   options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
-session Algebra = HOL +
+session "HOL-Algebra" in Algebra = HOL +
   description {*
     Author: Clemens Ballarin, started 24 September 1999
 
@@ -212,7 +212,7 @@
     "poly/Polynomial"    (*The full theory*)
   files "document/root.bib" "document/root.tex"
 
-session Auth = HOL +
+session "HOL-Auth" in Auth = HOL +
   options [document_graph]
   theories
     Auth_Shared
@@ -222,7 +222,7 @@
     "Guard/Auth_Guard_Public"
   files "document/root.tex"
 
-session UNITY = HOL +
+session "HOL-UNITY" in UNITY = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -268,17 +268,17 @@
     "ELT"
   files "document/root.tex"
 
-session Unix = HOL +
+session "HOL-Unix" in Unix = HOL +
   options [print_mode = "no_brackets,no_type_brackets"]
   theories Unix
   files "document/root.bib" "document/root.tex"
 
-session ZF = HOL +
+session "HOL-ZF" in ZF = HOL +
   description {* *}
   theories MainZF Games
   files "document/root.tex"
 
-session Imperative_HOL = HOL +
+session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   description {* *}
   options [document_graph, print_mode = "iff,no_brackets"]
   theories [document = false]
@@ -289,15 +289,15 @@
   theories Imperative_HOL_ex
   files "document/root.bib" "document/root.tex"
 
-session Decision_Procs = HOL +
+session "HOL-Decision_Procs" in Decision_Procs = HOL +
   options [condition = ISABELLE_POLYML, document = false]
   theories Decision_Procs
 
-session ex in "Proofs/ex" = "HOL-Proofs" +
+session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Hilbert_Classical
 
-session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
+session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   description {* Examples for program extraction in Higher-Order Logic *}
   options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   theories [document = false]
@@ -314,7 +314,7 @@
     Euclid
   files "document/root.bib" "document/root.tex"
 
-session Lambda in "Proofs/Lambda" = "HOL-Proofs" +
+session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Integer"
@@ -325,14 +325,14 @@
     WeakNorm
   files "document/root.bib" "document/root.tex"
 
-session Prolog = HOL +
+session "HOL-Prolog" in Prolog = HOL +
   description {*
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   *}
   options [document = false]
   theories Test Type
 
-session MicroJava = HOL +
+session "HOL-MicroJava" in MicroJava = HOL +
   options [document_graph]
   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   theories MicroJava
@@ -341,16 +341,16 @@
     "document/root.bib"
     "document/root.tex"
 
-session "MicroJava-skip_proofs" in MicroJava = HOL +
+session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
   options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
   theories MicroJava
 
-session NanoJava = HOL +
+session "HOL-NanoJava" in NanoJava = HOL +
   options [document_graph]
   theories Example
   files "document/root.bib" "document/root.tex"
 
-session Bali = HOL +
+session "HOL-Bali" in Bali = HOL +
   options [document_graph]
   theories
     AxExample
@@ -359,7 +359,7 @@
     Trans
   files "document/root.tex"
 
-session IOA = HOL +
+session "HOL-IOA" in IOA = HOL +
   description {*
     Author:     Tobias Nipkow & Konrad Slind
     Copyright   1994  TU Muenchen
@@ -388,7 +388,7 @@
   options [document = false]
   theories Solve
 
-session Lattice = HOL +
+session "HOL-Lattice" in Lattice = HOL +
   description {*
     Author:     Markus Wenzel, TU Muenchen
 
@@ -397,7 +397,7 @@
   theories CompleteLattice
   files "document/root.tex"
 
-session ex = HOL +
+session "HOL-ex" in ex = HOL +
   description {* Miscellaneous examples for Higher-Order Logic. *}
   options [timeout = 3600, condition = ISABELLE_POLYML]
   theories [document = false]
@@ -483,7 +483,7 @@
 *)
   files "document/root.bib" "document/root.tex"
 
-session Isar_Examples = HOL +
+session "HOL-Isar_Examples" in Isar_Examples = HOL +
   description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
@@ -509,35 +509,35 @@
     "document/root.tex"
     "document/style.tex"
 
-session SET_Protocol = HOL +
+session "HOL-SET_Protocol" in SET_Protocol = HOL +
   options [document_graph]
   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   theories SET_Protocol
   files "document/root.tex"
 
-session Matrix_LP = HOL +
+session "HOL-Matrix_LP" in Matrix_LP = HOL +
   options [document_graph]
   theories Cplex
   files "document/root.tex"
 
-session TLA = HOL +
+session "HOL-TLA" in TLA = HOL +
   description {* The Temporal Logic of Actions *}
   options [document = false]
   theories TLA
 
-session Inc in "TLA/Inc" = "HOL-TLA" +
+session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   options [document = false]
   theories Inc
 
-session Buffer in "TLA/Buffer" = "HOL-TLA" +
+session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   options [document = false]
   theories DBuffer
 
-session Memory in "TLA/Memory" = "HOL-TLA" +
+session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   options [document = false]
   theories MemoryImplementation
 
-session TPTP = HOL +
+session "HOL-TPTP" in TPTP = HOL +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Nik Sultana, University of Cambridge
@@ -555,7 +555,7 @@
   theories [proofs = 0]  (* FIXME !? *)
     ATP_Problem_Import
 
-session Multivariate_Analysis = HOL +
+session "HOL-Multivariate_Analysis" in Multivariate_Analysis = HOL +
   options [document_graph]
   theories
     Multivariate_Analysis
@@ -564,7 +564,7 @@
     "Integration.certs"
     "document/root.tex"
 
-session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
+session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   options [document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
@@ -576,45 +576,45 @@
     "ex/Koepf_Duermuth_Countermeasure"
   files "document/root.tex"
 
-session Nominal (main) = HOL +
+session "HOL-Nominal" (main) in Nominal = HOL +
   options [document = false]
   theories Nominal
 
-session Examples in "Nominal/Examples" = "HOL-Nominal" +
+session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   theories Nominal_Examples
   theories [quick_and_dirty] VC_Condition
 
-session Word = HOL +
+session "HOL-Word" in Word = HOL +
   options [document_graph]
   theories Word
   files "document/root.bib" "document/root.tex"
 
-session Examples in "Word/Examples" = "HOL-Word" +
+session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   options [document = false]
   theories WordExamples
 
-session Statespace = HOL +
+session "HOL-Statespace" in Statespace = HOL +
   theories StateSpaceEx
   files "document/root.tex"
 
-session NSA = HOL +
+session "HOL-NSA" in NSA = HOL +
   options [document_graph]
   theories Hypercomplex
   files "document/root.tex"
 
-session Examples in "NSA/Examples" = "HOL-NSA" +
+session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   options [document = false]
   theories NSPrimes
 
-session Mirabelle = HOL +
+session "HOL-Mirabelle" in Mirabelle = HOL +
   options [document = false]
   theories Mirabelle_Test
 
-session ex in "Mirabelle/ex" = "HOL-Mirabelle" +
+session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   theories Ex
 
-session SMT_Examples = "HOL-Word" +
+session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]
   theories
     SMT_Tests
@@ -624,11 +624,11 @@
     "SMT_Examples.certs"
     "SMT_Tests.certs"
 
-session "HOL-Boogie"! in "Boogie" = "HOL-Word" +
+session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   options [document = false]
   theories Boogie
 
-session Examples in "Boogie/Examples" = "HOL-Boogie" +
+session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   options [document = false]
   theories
     Boogie_Max_Stepwise
@@ -643,11 +643,11 @@
     "VCC_Max.b2i"
     "VCC_Max.certs"
 
-session "HOL-SPARK"! in "SPARK" = "HOL-Word" +
+session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   options [document = false]
   theories SPARK
 
-session Examples in "SPARK/Examples" = "HOL-SPARK" +
+session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   options [document = false]
   theories
     "Gcd/Greatest_Common_Divisor"
@@ -700,7 +700,7 @@
     "RIPEMD-160/rmd/s_r.rls"
     "RIPEMD-160/rmd/s_r.siv"
 
-session Manual in "SPARK/Manual" = "HOL-SPARK" +
+session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   options [show_question_marks = false]
   theories
     Example_Verification
@@ -733,11 +733,11 @@
     "simple_greatest_common_divisor/g_c_d.rls"
     "simple_greatest_common_divisor/g_c_d.siv"
 
-session Mutabelle = HOL +
+session "HOL-Mutabelle" in Mutabelle = HOL +
   options [document = false]
   theories MutabelleExtra
 
-session Quickcheck_Examples = HOL +
+session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   options [timeout = 3600, document = false]
   theories
     Quickcheck_Examples
@@ -749,14 +749,14 @@
   theories [condition = ISABELLE_GHC]
     Quickcheck_Narrowing_Examples
 
-session Quickcheck_Benchmark = HOL +
+session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
     Find_Unused_Assms_Examples
     Needham_Schroeder_No_Attacker_Example
     Needham_Schroeder_Guided_Attacker_Example
     Needham_Schroeder_Unguided_Attacker_Example
 
-session Quotient_Examples = HOL +
+session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
@@ -772,7 +772,7 @@
     Quotient_Rat
     Lift_DList
 
-session Predicate_Compile_Examples = HOL +
+session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   options [document = false]
   theories
     Examples
@@ -795,7 +795,7 @@
   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
     Reg_Exp_Example
 
-session HOLCF! (main) = HOL +
+session HOLCF (main) in HOLCF = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
@@ -812,23 +812,23 @@
     HOLCF
   files "document/root.tex"
 
-session Tutorial in "HOLCF/Tutorial" = HOLCF +
+session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   theories
     Domain_ex
     Fixrec_ex
     New_Domain
   files "document/root.tex"
 
-session Library in "HOLCF/Library" = HOLCF +
+session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   options [document = false]
   theories HOLCF_Library
 
-session IMP in "HOLCF/IMP" = HOLCF +
+session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   options [document = false]
   theories HoareEx
   files "document/root.tex"
 
-session ex in "HOLCF/ex" = HOLCF +
+session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   description {* Misc HOLCF examples *}
   options [document = false]
   theories
@@ -844,14 +844,14 @@
     Letrec
     Pattern_Match
 
-session FOCUS in "HOLCF/FOCUS" = HOLCF +
+session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   options [document = false]
   theories
     Fstreams
     FOCUS
     Buffer_adm
 
-session IOA! in "HOLCF/IOA" = HOLCF +
+session IOA in "HOLCF/IOA" = HOLCF +
   description {*
     Author:     Olaf Mueller
 
@@ -860,7 +860,7 @@
   options [document = false]
   theories "meta_theory/Abstraction"
 
-session ABP in "HOLCF/IOA/ABP" = IOA +
+session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   description {*
     Author:     Olaf Mueller
 
@@ -869,7 +869,7 @@
   options [document = false]
   theories Correctness
 
-session NTP in "HOLCF/IOA/NTP" = IOA +
+session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
   description {*
     Author:     Tobias Nipkow & Konrad Slind
 
@@ -879,7 +879,7 @@
   options [document = false]
   theories Correctness
 
-session Storage in "HOLCF/IOA/Storage" = IOA +
+session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   description {*
     Author:     Olaf Mueller
 
@@ -888,7 +888,7 @@
   options [document = false]
   theories Correctness
 
-session ex in "HOLCF/IOA/ex" = IOA +
+session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   description {*
     Author:     Olaf Mueller
   *}
@@ -897,7 +897,7 @@
     TrivEx
     TrivEx2
 
-session Datatype_Benchmark = HOL +
+session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
   description {* Some rather large datatype examples (from John Harrison). *}
   options [document = false]
   theories [condition = ISABELLE_FULL_TEST, timing]
@@ -906,7 +906,7 @@
     SML
     Verilog
 
-session Record_Benchmark = HOL +
+session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   description {* Some benchmark on large record. *}
   options [document = false]
   theories [condition = ISABELLE_FULL_TEST, timing]
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/LCF/ROOT
--- a/src/LCF/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/LCF/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session LCF! in "." = Pure +
+session LCF = Pure +
   description {*
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
@@ -6,7 +6,7 @@
   options [document = false]
   theories LCF
 
-session ex = LCF +
+session "LCF-ex" in ex = LCF +
   description {*
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Pure/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session RAW in "." =
+session RAW =
   files
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
@@ -19,7 +19,7 @@
     "ML-Systems/unsynchronized.ML"
     "ML-Systems/use_context.ML"
 
-session Pure in "." =
+session Pure =
   theories Pure
   files
     "General/exn.ML"
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Aug 08 17:49:56 2012 +0200
@@ -23,10 +23,9 @@
   // external version
   sealed case class Session_Entry(
     pos: Position.T,
-    base_name: String,
-    this_name: Boolean,
+    name: String,
     groups: List[String],
-    path: Option[String],
+    path: String,
     parent: Option[String],
     description: String,
     options: List[Options.Spec],
@@ -51,26 +50,11 @@
   def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
       : (String, Session_Info) =
     try {
-      if (entry.base_name == "") error("Bad session name")
+      val name = entry.name
 
-      val full_name =
-        if (is_pure(entry.base_name)) {
-          if (entry.parent.isDefined) error("Illegal parent session")
-          else entry.base_name
-        }
-        else
-          entry.parent match {
-            case None => error("Missing parent session")
-            case Some(parent_name) =>
-              if (entry.this_name) entry.base_name
-              else parent_name + "-" + entry.base_name
-          }
-
-      val path =
-        entry.path match {
-          case Some(p) => Path.explode(p)
-          case None => Path.basic(entry.base_name)
-        }
+      if (name == "") error("Bad session name")
+      if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+      if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
       val session_options = options ++ entry.options
 
@@ -78,19 +62,18 @@
         entry.theories.map({ case (opts, thys) =>
           (session_options ++ opts, thys.map(Path.explode(_))) })
       val files = entry.files.map(Path.explode(_))
-      val entry_digest =
-        SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
+      val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
 
       val info =
-        Session_Info(select, entry.pos, entry.groups, dir + path, entry.parent, entry.description,
-          session_options, theories, files, entry_digest)
+        Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
+          entry.parent, entry.description, session_options, theories, files, entry_digest)
 
-      (full_name, info)
+      (name, info)
     }
     catch {
       case ERROR(msg) =>
         error(msg + "\nThe error(s) above occurred in session entry " +
-          quote(entry.base_name) + Position.str_of(entry.pos))
+          quote(entry.name) + Position.str_of(entry.pos))
     }
 
 
@@ -175,7 +158,7 @@
   private val FILES = "files"
 
   lazy val root_syntax =
-    Outer_Syntax.init() + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
 
   private object Parser extends Parse.Parser
@@ -193,15 +176,14 @@
           { case _ ~ (x ~ y) => (x, y) }
 
       ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
-        (keyword("!") ^^^ true | success(false)) ~
         (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
-        (opt(keyword(IN) ~! path ^^ { case _ ~ x => x })) ~
+        (keyword(IN) ~! path ^^ { case _ ~ x => x } | success(".")) ~
         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
         rep(theories) ~
         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
-          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
+          { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(pos, a, b, c, d, e, f, g, h) }
     }
 
     def parse_entries(root: Path): List[Session_Entry] =
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/Sequents/ROOT
--- a/src/Sequents/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Sequents/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session Sequents! in "." = Pure +
+session Sequents = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
@@ -16,7 +16,7 @@
     S4
     S43
 
-session LK = Sequents +
+session "Sequents-LK" in LK = Sequents +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/Tools/WWW_Find/ROOT
--- a/src/Tools/WWW_Find/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Tools/WWW_Find/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,3 +1,3 @@
-session WWW_Find in "." = Pure +
+session WWW_Find = Pure +
   theories [condition = ISABELLE_POLYML] WWW_Find
 
diff -r f3bbb9ca57d6 -r f8c1a5b9488f src/ZF/ROOT
--- a/src/ZF/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/ZF/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session ZF! in "." = Pure +
+session ZF = Pure +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
@@ -13,7 +13,7 @@
     Main_ZFC
   files "document/root.tex"
 
-session AC = ZF +
+session "ZF-AC" in AC = ZF +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
@@ -34,7 +34,7 @@
     DC
   files "document/root.tex" "document/root.bib"
 
-session Coind = ZF +
+session "ZF-Coind" in Coind = ZF +
   description {*
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
@@ -53,13 +53,13 @@
   options [document = false]
   theories ECR
 
-session Constructible = ZF +
+session "ZF-Constructible" in Constructible = ZF +
   description {* Inner Models, Absoluteness and Consistency Proofs. *}
   options [document_graph]
   theories DPow_absolute AC_in_L Rank_Separation
   files "document/root.tex" "document/root.bib"
 
-session IMP = ZF +
+session "ZF-IMP" in IMP = ZF +
   description {*
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
@@ -77,7 +77,7 @@
   theories Equiv
   files "document/root.tex" "document/root.bib"
 
-session Induct = ZF +
+session "ZF-Induct" in Induct = ZF +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
@@ -108,7 +108,7 @@
     Primrec         (*Primitive recursive functions*)
   files "document/root.tex"
 
-session Resid = ZF +
+session "ZF-Resid" in Resid = ZF +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
@@ -124,7 +124,7 @@
   options [document = false]
   theories Confluence
 
-session UNITY = ZF +
+session "ZF-UNITY" in UNITY = ZF +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -142,7 +142,7 @@
     (*Prefix relation; the Allocator example*)
     Distributor Merge ClientImpl AllocImpl
 
-session ex = ZF +
+session "ZF-ex" in ex = ZF +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge