# HG changeset patch
# User wenzelm
# Date 1357911224 -3600
# Node ID 133a38b7ceaf9d12733285a07664c8376db95422
# Parent  bfbb96177a255584e7e26ec3815703d24ef70af3
discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;

diff -r bfbb96177a25 -r 133a38b7ceaf src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jan 11 13:24:22 2013 +0100
+++ b/src/HOL/ROOT	Fri Jan 11 14:33:44 2013 +0100
@@ -8,24 +8,6 @@
     "document/root.bib"
     "document/root.tex"
 
-session "HOL-Base" = Pure +
-  description {* Raw HOL base, with minimal tools *}
-  options [document = false]
-  theories HOL
-
-session "HOL-Plain" = Pure +
-  description {* HOL side-entry after bootstrap of many tools and packages *}
-  options [document = false]
-  theories Plain
-
-session "HOL-Main" = Pure +
-  description {* HOL side-entry for Main only, without Complex_Main *}
-  options [document = false]
-  theories Main
-  files
-    "Tools/Quickcheck/Narrowing_Engine.hs"
-    "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
-
 session "HOL-Proofs" = Pure +
   description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]