equal
deleted
inserted
replaced
125 the current simpset. |
125 the current simpset. |
126 *} |
126 *} |
127 |
127 |
128 section {* Contexts (TBD) *} |
128 section {* Contexts (TBD) *} |
129 |
129 |
130 ML_command "ProofContext.debug := true" |
130 ML{*ProofContext.debug*} |
131 ML_command "ProofContext.verbose := true" |
131 ML{*ProofContext.verbose*} |
132 |
132 |
133 |
133 |
134 section {* Local Theories (TBD) *} |
134 section {* Local Theories (TBD) *} |
135 |
135 |
136 text {* |
136 text {* |
274 text {* |
274 text {* |
275 \footnote{\bf FIXME: Explain the following better; maybe put in a separate |
275 \footnote{\bf FIXME: Explain the following better; maybe put in a separate |
276 section and link with the comment in the antiquotation section.} |
276 section and link with the comment in the antiquotation section.} |
277 |
277 |
278 Occasionally you have to calculate what the ``base'' name of a given |
278 Occasionally you have to calculate what the ``base'' name of a given |
279 constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or |
279 constant is. For this you can use the function @{ML_ind Long_Name.base_name}. For example: |
280 @{ML_ind Long_Name.base_name}. For example: |
280 |
281 |
281 @{ML_response [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""} |
282 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} |
|
283 |
|
284 The difference between both functions is that @{ML extern_const in Sign} returns |
|
285 the smallest name that is still unique, whereas @{ML base_name in Long_Name} always |
|
286 strips off all qualifiers. |
|
287 |
282 |
288 \begin{readmore} |
283 \begin{readmore} |
289 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |
284 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"}; |
290 functions about signatures in @{ML_file "Pure/sign.ML"}. |
285 functions about signatures in @{ML_file "Pure/sign.ML"}. |
291 \end{readmore} |
286 \end{readmore} |