author | wenzelm |
Thu, 08 Mar 2012 21:40:15 +0100 | |
changeset 46840 | 42e32c777581 |
parent 46839 | f7232c078fa5 |
child 46843 | 8d5d255bf89c |
--- a/src/Pure/PIDE/xml.ML Thu Mar 08 21:36:36 2012 +0100 +++ b/src/Pure/PIDE/xml.ML Thu Mar 08 21:40:15 2012 +0100 @@ -3,7 +3,7 @@ Author: Stefan Berghofer Author: Makarius -Untyped XML trees and basic data representation. +Untyped XML trees and representation of ML values. *) signature XML_DATA_OPS =