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.
binding replaces Binding.T
authorhaftmann
Thu, 22 Jan 2009 09:08:58 +0100
changeset 29616 e8c121c64475
parent 29615 24a58ae5dc0e
child 29617 b36bcbc1be3a
binding replaces Binding.T
NEWS file | annotate | diff | comparison | revisions 
--- a/NEWS	Thu Jan 22 09:04:56 2009 +0100
+++ b/NEWS	Thu Jan 22 09:08:58 2009 +0100
@@ -72,13 +72,13 @@
 
     class foo = ...     instead of      class foo = type + ...
 
-* Type Binding.T gradually replaces formerly used type bstring for names
+* Type binding gradually replaces formerly used type bstring for names
 to be bound.  Name space interface for declarations has been simplified:
 
   NameSpace.declare: NameSpace.naming
-    -> Binding.T -> NameSpace.T -> string * NameSpace.T
+    -> binding -> NameSpace.T -> string * NameSpace.T
   NameSpace.bind: NameSpace.naming
-    -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
+    -> binding * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
          (*exception Symtab.DUP*)
 
 See further modules src/Pure/General/binding.ML and
isabelle