src/HOL/ROOT

--- a/src/HOL/ROOT	Fri Mar 03 23:21:24 2017 +0100
+++ b/src/HOL/ROOT	Thu Mar 02 21:16:02 2017 +0100
@@ -297,7 +297,9 @@
     "~~/src/HOL/Number_Theory/Primes"
     "~~/src/HOL/Library/Permutation"
   theories
-    (*** New development, based on explicit structures ***)
+    (* Orders and Lattices *)
+    Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
+
     (* Groups *)
     FiniteProduct        (* Product operator for commutative groups *)
     Sylow                (* Sylow's theorem *)