src/HOL/Library/Library.thy
changeset 56020 f92479477c52
parent 55159 608c157d743d
child 56415 f61a0f7cbde5
--- a/src/HOL/Library/Library.thy	Mon Mar 10 17:14:57 2014 +0100
+++ b/src/HOL/Library/Library.thy	Mon Mar 10 20:04:40 2014 +0100
@@ -7,7 +7,6 @@
   BNF_Decl
   Boolean_Algebra
   Char_ord
-  Continuity
   ContNotDenum
   Convex
   Countable
@@ -41,6 +40,7 @@
   Numeral_Type
   OptionalSugar
   Option_ord
+  Order_Continuity
   Parallel
   Permutation
   Permutations