discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;
authorwenzelm
Fri, 11 Jan 2013 14:33:44 +0100
changeset 50833 133a38b7ceaf
parent 50832 bfbb96177a25
child 50834 506342881c33
discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;
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]