src/Pure/General/markup.scala
changeset 38887 1261481ef5e5
parent 38872 26c505765024
child 39168 e3ac771235f7
equal deleted inserted replaced
38886:9210cf2b4869 38887:1261481ef5e5
    67   val KIND = "kind"
    67   val KIND = "kind"
    68 
    68 
    69 
    69 
    70   /* formal entities */
    70   /* formal entities */
    71 
    71 
       
    72   val BINDING = "binding"
    72   val ENTITY = "entity"
    73   val ENTITY = "entity"
    73   val DEF = "def"
    74   val DEF = "def"
    74   val REF = "ref"
    75   val REF = "ref"
    75 
    76 
    76 
    77