src/HOL/NSA/ROOT.ML
author bulwahn
Thu, 19 Nov 2009 08:25:53 +0100
changeset 33754 f2957bd46faf
parent 33615 261abc2e3155
permissions -rw-r--r--
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler

use_thys ["Hypercomplex"];