# HG changeset patch
# User wenzelm
# Date 1343731081 -7200
# Node ID 6004f45756456952f73567fc77bfa4575052b4e9
# Parent  232652ac346e63f0f93cba06b661ccb71255f6e2
renamed session TLA to HOL-TLA to avoid clash with AFP;

diff -r 232652ac346e -r 6004f4575645 src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jul 30 20:43:07 2012 +0200
+++ b/src/HOL/ROOT	Tue Jul 31 12:38:01 2012 +0200
@@ -515,20 +515,20 @@
   theories Cplex
   files "document/root.tex"
 
-session TLA! = HOL +
+session TLA = HOL +
   description {* The Temporal Logic of Actions *}
   options [document = false]
   theories TLA
 
-session Inc in "TLA/Inc" = TLA +
+session Inc in "TLA/Inc" = "HOL-TLA" +
   options [document = false]
   theories Inc
 
-session Buffer in "TLA/Buffer" = TLA +
+session Buffer in "TLA/Buffer" = "HOL-TLA" +
   options [document = false]
   theories DBuffer
 
-session Memory in "TLA/Memory" = TLA +
+session Memory in "TLA/Memory" = "HOL-TLA" +
   options [document = false]
   theories MemoryImplementation