# HG changeset patch # User wenzelm # Date 852566529 -3600 # Node ID 09634c9cbf3ce0fa867190f94c1e7aa8f927b083 # Parent 273580d5c04020b87cbf9179aabb1ab1a46d37c1 added stamp util; diff -r 273580d5c040 -r 09634c9cbf3c src/Pure/library.ML --- a/src/Pure/library.ML Fri Jan 03 15:25:51 1997 +0100 +++ b/src/Pure/library.ML Mon Jan 06 17:02:09 1997 +0100 @@ -45,6 +45,13 @@ +(** stamps **) + +type stamp = unit ref; +val stamp: unit -> stamp = ref; + + + (** options **) datatype 'a option = None | Some of 'a;