| author | wenzelm |
| Thu, 17 Dec 2009 15:38:58 +0100 | |
| changeset 34097 | 9274a44358c4 |
| parent 33446 | 153a27370a42 |
| permissions | -rw-r--r-- |
|
33446
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
1 |
(benchmark Isabelle |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
2 |
:extrasorts ( T1) |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
3 |
:extrafuns ( |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
4 |
(uf_1 Real) |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
5 |
) |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
6 |
:assumption (not (= uf_1 0.0)) |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
7 |
:assumption (not (not (= (+ uf_1 uf_1) (* (ite (or (< 1.0 (ite (< uf_1 0.0) (~ uf_1) uf_1)) (not (< 1.0 (ite (< uf_1 0.0) (~ uf_1) uf_1)))) 4.0 2.0) uf_1)))) |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
8 |
:formula true |
|
153a27370a42
handle let expressions inside terms by unfolding (instead of raising an exception),
boehmes
parents:
diff
changeset
|
9 |
) |