src/HOL/Import/Generate-HOL/ROOT.ML
author wenzelm
Mon, 13 Jun 2011 23:09:01 +0200
changeset 43376 0f6880c1c759
parent 41589 bbd861837ebc
child 44367 74c08021ab2e
permissions -rw-r--r--
some direct text foreground painting, instead of token marking; common snapshot for all text area painters (NOT gutter etc.) tuned;

use_thy "GenHOL4Prob";
use_thy "GenHOL4Vec";
use_thy "GenHOL4Word32";