equal
deleted
inserted
replaced
55 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
55 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
56 interface instead. |
56 interface instead. |
57 |
57 |
58 |
58 |
59 *** Pure *** |
59 *** Pure *** |
|
60 |
|
61 * Type Binding.T gradually replaces formerly used type bstring for names |
|
62 to be bound. Name space interface for declarations has been simplified: |
|
63 |
|
64 NameSpace.declare: NameSpace.naming |
|
65 -> Binding.T -> NameSpace.T -> string * NameSpace.T |
|
66 NameSpace.bind: NameSpace.naming |
|
67 -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table |
|
68 (*exception Symtab.DUP*) |
|
69 |
|
70 See further modules src/Pure/General/binding.ML and |
|
71 src/Pure/General/name_space.ML |
60 |
72 |
61 * Module moves in repository: |
73 * Module moves in repository: |
62 src/Pure/Tools/value.ML ~> src/Tools/ |
74 src/Pure/Tools/value.ML ~> src/Tools/ |
63 src/Pure/Tools/quickcheck.ML ~> src/Tools/ |
75 src/Pure/Tools/quickcheck.ML ~> src/Tools/ |
64 |
76 |