src/HOL/Import/ImportRecorder.thy
author blanchet
Tue, 07 Dec 2010 11:56:01 +0100
changeset 41045 2a41709f34c1
parent 20594 b80c4a5cd018
permissions -rw-r--r--
use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets

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