# HG changeset patch
# User nipkow
# Date 1106753984 -3600
# Node ID 7e12ad2f66725d0321e067528d59d987fe3d0680
# Parent  f5d22f504ab9685e75b4ed6740b2ebb191fd8420
added OptionalSugar

diff -r f5d22f504ab9 -r 7e12ad2f6672 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Jan 26 13:50:59 2005 +0100
+++ b/src/HOL/Library/Library.thy	Wed Jan 26 16:39:44 2005 +0100
@@ -10,6 +10,7 @@
   NatPair
   Nat_Infinity
   Nested_Environment
+  OptionalSugar
   Permutation
   Primes
   Quotient