Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
specific output setup is not supposed to intrude regular import theory
authorhaftmann
Mon, 05 Jun 2017 15:59:45 +0200
changeset 66015 70643edecb7a
parent 66014 2f45f4abf0a9
child 66016 39d9a59d8d94
specific output setup is not supposed to intrude regular import theory
src/HOL/Library/Library.thy file | annotate | diff | comparison | revisions
src/HOL/ROOT file | annotate | diff | comparison | revisions 
--- 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
--- 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*)
isabelle