doc-src/TutorialI/CodeGen/ROOT.ML
author blanchet
Wed, 04 May 2011 15:35:05 +0200
changeset 42677 25496cd3c199
parent 9834 109b11c4e77e
permissions -rw-r--r--
monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.

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