# HG changeset patch
# User haftmann
# Date 1496671185 -7200
# Node ID 70643edecb7af261a23a82691080f90516280bd2
# Parent  2f45f4abf0a96cdd386a699c91cf719c9284a503
specific output setup is not supposed to intrude regular import theory

diff -r 2f45f4abf0a9 -r 70643edecb7a src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Library/Library.thy	Mon Jun 05 15:59:45 2017 +0200
@@ -48,7 +48,6 @@
   Nonpos_Ints
   Numeral_Type
   Omega_Words_Fun
-  OptionalSugar
   Option_ord
   Order_Continuity
   Parallel
diff -r 2f45f4abf0a9 -r 70643edecb7a src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/ROOT	Mon Jun 05 15:59:45 2017 +0200
@@ -52,6 +52,8 @@
     DAList_Multiset
     RBT_Mapping
     RBT_Set
+    (*printing modifications*)
+    OptionalSugar
     (*prototypic tools*)
     Predicate_Compile_Quickcheck
     (*legacy tools*)