src/Pure/General/position.ML
2007-07-10 wenzelm 2007-07-10 Markup.enclose;
2007-07-10 wenzelm 2007-07-10 Markup.output;
2007-07-09 wenzelm 2007-07-09 replaced name by file (unquoted); str_of: markup; misc cleanup;
2007-07-07 wenzelm 2007-07-07 added property conversions; tuned;
2007-01-22 aspinall 2007-01-22 Add line_of, name_of destructors.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2000-05-05 wenzelm 2000-05-05 GPLed;
1999-01-13 wenzelm 1999-01-13 fixed titles;
1998-06-10 wenzelm 1998-06-10 moved Thy/position.ML to General/position.ML;