src/HOL/HOLCF/Library/ROOT.ML
author huffman
Sun, 19 Dec 2010 17:37:19 -0800
changeset 41292 2b7bc8d9fd6e
parent 40774 0437dbc127b3
permissions -rw-r--r--
use deflations over type 'udom u' to represent predomains; removed now-unnecessary class liftdomain;

use_thys ["HOLCF_Library"];