equal
deleted
inserted
replaced
285 functions about signatures in @{ML_file "Pure/sign.ML"}. |
285 functions about signatures in @{ML_file "Pure/sign.ML"}. |
286 \end{readmore} |
286 \end{readmore} |
287 *} |
287 *} |
288 |
288 |
289 text {* |
289 text {* |
290 @{ML_ind "Binding.str_of"} returns the string with markup; |
|
291 @{ML_ind "Binding.name_of"} returns the string without markup |
290 @{ML_ind "Binding.name_of"} returns the string without markup |
292 |
291 |
293 @{ML_ind "Binding.conceal"} |
292 @{ML_ind "Binding.conceal"} |
294 *} |
293 *} |
295 |
294 |