src/HOL/Mirabelle/ROOT.ML
author kuncar
Thu, 26 Apr 2012 14:11:13 +0200
changeset 47779 5a10e24fe7ab
parent 33615 261abc2e3155
permissions -rw-r--r--
tuned; don't generate abs code if quotient_type is used

use_thys ["Mirabelle_Test"];