doc-src/TutorialI/Advanced/ROOT.ML
author wenzelm
Tue, 03 Mar 2009 14:16:05 +0100
changeset 30213 3951aab916fd
parent 25281 8d309beb66d6
child 48506 af1dabad14c0
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 "simp";