equal
deleted
inserted
replaced
136 |
136 |
137 These specifications may be also used in a locale context. Then the |
137 These specifications may be also used in a locale context. Then the |
138 constants being introduced depend on certain fixed parameters, and the |
138 constants being introduced depend on certain fixed parameters, and the |
139 constant name is qualified by the locale base name. An internal |
139 constant name is qualified by the locale base name. An internal |
140 abbreviation takes care for convenient input and output, making the |
140 abbreviation takes care for convenient input and output, making the |
141 parameters implicit and using the original short name. See |
141 parameters implicit and using the original short name. See also |
142 HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
142 HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
143 entities from a monomorphic theory. |
143 entities from a monomorphic theory. |
144 |
144 |
145 Presently, abbreviations are only available 'in' a target locale, but |
145 Presently, abbreviations are only available 'in' a target locale, but |
146 not inherited by general import expressions. |
146 not inherited by general import expressions. |