# HG changeset patch
# User haftmann
# Date 1396684867 -7200
# Node ID f61a0f7cbde5c3a213b2b9d6df3e40fdcdd483b2
# Parent  c1bbd3e22226addd8b08f440afee07daa341785e
proper inclusion into library

diff -r c1bbd3e22226 -r f61a0f7cbde5 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Sat Apr 05 01:04:46 2014 +0100
+++ b/src/HOL/Library/Library.thy	Sat Apr 05 10:01:07 2014 +0200
@@ -33,6 +33,7 @@
   Lattice_Algebras
   Lattice_Syntax
   ListVector
+  Lubs_Glbs
   Kleene_Algebra
   Mapping
   Monad_Syntax