doc-src/TutorialI/CodeGen/ROOT.ML
author wenzelm
Tue, 03 Mar 2009 14:16:05 +0100
changeset 30213 3951aab916fd
parent 9834 109b11c4e77e
permissions -rw-r--r--
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);

use "../settings.ML";
use_thy "CodeGen";