| author | boehmes |
| Tue, 20 Oct 2009 10:11:30 +0200 | |
| changeset 33006 | 39f73a59e855 |
| permissions | -rw-r--r-- |
| boehmes@33006 | 1 |
(benchmark Isabelle |
| boehmes@33006 | 2 |
:extrafuns ( |
| boehmes@33006 | 3 |
(uf_1 Real) |
| boehmes@33006 | 4 |
(uf_2 Real) |
| boehmes@33006 | 5 |
) |
| boehmes@33006 | 6 |
:assumption (not (<= (ite (< (+ uf_1 uf_2) 0.0) (~ (+ uf_1 uf_2)) (+ uf_1 uf_2)) (+ (ite (< uf_1 0.0) (~ uf_1) uf_1) (ite (< uf_2 0.0) (~ uf_2) uf_2)))) |
| boehmes@33006 | 7 |
:formula true |
| boehmes@33006 | 8 |
) |