src/HOL/ROOT

--- a/src/HOL/ROOT	Sat Dec 10 17:22:47 2016 +0100
+++ b/src/HOL/ROOT	Mon Dec 12 17:40:06 2016 +0100
@@ -38,7 +38,6 @@
     Predicate_Compile_Quickcheck
     Prefix_Order
     Rewrite
-    Types_To_Sets
     (*conflicting type class instantiations*)
     List_lexord
     Sublist_Order
@@ -1018,6 +1017,17 @@
   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
     Reg_Exp_Example
 
+session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
+  description {*
+    Experimental extension of Higher-Order Logic to allow translation of types to sets.
+  *}
+  options [document = false]
+  theories
+    Types_To_Sets
+    "Examples/Prerequisites"
+    "Examples/Finite"
+    "Examples/T2_Spaces"
+
 session HOLCF (main timing) in HOLCF = HOL +
   description {*
     Author:     Franz Regensburger