src/Pure/Isar/document_structure.scala
changeset 80225 d9ff4296e3b7
parent 78912 ff4496b25197
equal deleted inserted replaced
80224:db92e0b6a11a 80225:d9ff4296e3b7