src/HOL/SPARK/ROOT.ML
author bulwahn
Wed, 30 Mar 2011 09:44:16 +0200
changeset 42159 234ec7011e5d
parent 41561 d1318f3c86ba
permissions -rw-r--r--
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     1
use_thys ["SPARK"];