doc-src/IsarRef/Thy/ROOT-HOLCF.ML
author haftmann
Wed, 19 May 2010 12:35:20 +0200
changeset 36985 41c5d4002f60
parent 32833 f3716d1a2e48
child 37216 3165bc303f66
permissions -rw-r--r--
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term

Unsynchronized.set ThyOutput.source;
use "../../antiquote_setup.ML";

use_thy "HOLCF_Specific";