src/HOL/Import/ImportRecorder.thy
author wenzelm
Mon, 13 Jun 2011 23:09:01 +0200
changeset 43376 0f6880c1c759
parent 20594 b80c4a5cd018
permissions -rw-r--r--
some direct text foreground painting, instead of token marking; common snapshot for all text area painters (NOT gutter etc.) tuned;

theory ImportRecorder imports Main 
uses  "seq.ML" "scan.ML" "mono_seq.ML" "mono_scan.ML" "lazy_seq.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
begin
end