doc-src/TutorialI/CodeGen/ROOT.ML
author paulson
Tue, 09 Jan 2007 18:12:59 +0100
changeset 22044 6c0702a96076
parent 9834 109b11c4e77e
permissions -rw-r--r--
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded into the rest of the proof.

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