ProgTutorial/FirstSteps.thy
changeset 258 03145998190b
parent 257 ce0f60d0351e
child 260 5accec94b6df
equal deleted inserted replaced
257:ce0f60d0351e 258:03145998190b
  1007   "@{type_name \"list\"}" "\"List.list\""}
  1007   "@{type_name \"list\"}" "\"List.list\""}
  1008 
  1008 
  1009   (FIXME: Explain the following better.)
  1009   (FIXME: Explain the following better.)
  1010 
  1010 
  1011   Occasionally you have to calculate what the ``base'' name of a given
  1011   Occasionally you have to calculate what the ``base'' name of a given
  1012   constant is. For this you can use the function @{ML [index] extern_const in Sign} or
  1012   constant is. For this you can use the function @{ML [index] "Sign.extern_const"} or
  1013   @{ML base_name in Long_Name}. For example:
  1013   @{ML [index] Long_Name.base_name}. For example:
  1014 
  1014 
  1015   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
  1015   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
  1016 
  1016 
  1017   The difference between both functions is that @{ML extern_const in Sign} returns
  1017   The difference between both functions is that @{ML extern_const in Sign} returns
  1018   the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
  1018   the smallest name that is still unique, whereas @{ML base_name in Long_Name} always