# HG changeset patch # User berghofe # Date 1127671979 -7200 # Node ID 7daaa7fe9c96ffaf24dc0a42230497e1aa2aa487 # Parent 13d6a689efe9e29480ba84021dd1396d73c54397 Added ExecutableSet. diff -r 13d6a689efe9 -r 7daaa7fe9c96 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Sun Sep 25 20:12:26 2005 +0200 +++ b/src/HOL/Library/Library.thy Sun Sep 25 20:12:59 2005 +0200 @@ -5,6 +5,7 @@ BigO Continuity EfficientNat + ExecutableSet FuncSet Multiset NatPair