src/HOL/SMT/Examples/cert/z3_prop_05
author wenzelm
Sun, 27 Dec 2009 21:33:35 +0100
changeset 34187 7b659c1561f1
parent 33010 39f73a59e855
permissions -rw-r--r--
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);

(benchmark Isabelle
:extrasorts ( T1)
:extrapreds (
  (up_1)
  (up_2)
  (up_3)
  (up_4)
 )
:assumption (or (and up_1 up_2) (and up_3 up_4))
:assumption (not (or (and up_1 up_2) (and up_3 up_4)))
:formula true
)