src/HOL/SMT/Examples/cert/z3_bv_arith_02
author haftmann
Wed, 27 Jan 2010 14:02:52 +0100
changeset 34968 ceeffca32eb0
parent 33010 39f73a59e855
permissions -rw-r--r--
tuned structure; moved non-related quickcheck.setup to Code_Generator.thy

(benchmark Isabelle
:assumption (not (= bv27[4] bv11[4]))
:formula true
)