equal
deleted
inserted
replaced
58 * There is a new lexical item "float" with syntax ["-"] digit+ "." digit+, |
58 * There is a new lexical item "float" with syntax ["-"] digit+ "." digit+, |
59 without spaces. |
59 without spaces. |
60 |
60 |
61 |
61 |
62 *** Pure *** |
62 *** Pure *** |
|
63 |
|
64 * Type Binding.T gradually replaces formerly used type bstring for names |
|
65 to be bound. Name space interface for declarations has been simplified: |
|
66 |
|
67 NameSpace.declare: NameSpace.naming |
|
68 -> Binding.T -> NameSpace.T -> string * NameSpace.T |
|
69 NameSpace.bind: NameSpace.naming |
|
70 -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table |
|
71 (*exception Symtab.DUP*) |
|
72 |
|
73 See further modules src/Pure/General/binding.ML and |
|
74 src/Pure/General/name_space.ML |
63 |
75 |
64 * Module moves in repository: |
76 * Module moves in repository: |
65 src/Pure/Tools/value.ML ~> src/Tools/ |
77 src/Pure/Tools/value.ML ~> src/Tools/ |
66 src/Pure/Tools/quickcheck.ML ~> src/Tools/ |
78 src/Pure/Tools/quickcheck.ML ~> src/Tools/ |
67 |
79 |