src/HOL/Import/ImportRecorder.thy
author wenzelm
Thu, 02 Sep 2010 23:45:37 +0200
changeset 39045 30f3d9daaa3a
parent 20594 b80c4a5cd018
permissions -rw-r--r--
inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;

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